1 /-
2 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Zhouhang Zhou
5 -/
6
7 import measure_theory.ae_eq_fun
src └──────────────────────┘
8
9 /-!
10 # Integrable functions and `L¹` space
11
12 In the first part of this file, the predicate `integrable` is defined and basic properties of
13 integrable functions are proved.
14
15 In the second part, the space `L¹` of equivalence classes of integrable functions under the relation
16 of being almost everywhere equal is defined as a subspace of the space `L⁰`. See the file
17 `src/measure_theory/ae_eq_fun.lean` for information on `L⁰` space.
18
19 ## Notation
20
21 * `α →₁ β` is the type of `L¹` space, where `α` is a `measure_space` and `β` is a `normed_group` with
22 a `second_countable_topology`. `f : α →ₘ β` is a "function" in `L¹`. In comments, `[f]` is also used
23 to denote an `L¹` function.
24
25 `₁` can be typed as `\1`.
26
27 ## Main definitions
28
29 * Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`.
30 Then `f` is called `integrable` if `(∫⁻ a, nnnorm (f a)) < ⊤` holds.
31
32 * The space `L¹` is defined as a subspace of `L⁰` :
33 An `ae_eq_fun` `[f] : α →ₘ β` is in the space `L¹` if `edist [f] 0 < ⊤`, which means
34 `(∫⁻ a, edist (f a) 0) < ⊤` if we expand the definition of `edist` in `L⁰`.
35
36 ## Main statements
37
38 `L¹`, as a subspace, inherits most of the structures of `L⁰`.
39
40 ## Implementation notes
41
42 Maybe `integrable f` should be mean `(∫⁻ a, edist (f a) 0) < ⊤`, so that `integrable` and
43 `ae_eq_fun.integrable` are more aligned. But in the end one can use the lemma
44 `lintegral_nnnorm_eq_lintegral_edist : (∫⁻ a, nnnorm (f a)) = (∫⁻ a, edist (f a) 0)` to switch the
45 two forms.
46
47 ## Tags
48
49 integrable, function space, l1
50
51 -/
52
53 noncomputable theory
54 open_locale classical topological_space
55
56 set_option class.instance_max_depth 100
doc └──────────────────────┘
57
58 namespace measure_theory
59 open set lattice filter topological_space ennreal emetric
60
61 universes u v w
62 variables {α : Type u} [measure_space α]
id ┴ └───────────┘
src └───────────┘
typ ┴ └───────────┘
doc └───────────┘
63 variables {β : Type v} [normed_group β] {γ : Type w} [normed_group γ]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
64
65 /-- A function is `integrable` if the integral of its pointwise norm is less than infinity. -/
66 def integrable (f : α → β) : Prop := (∫⁻ a, nnnorm (f a)) < ⊤
id ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
src └┘ ┴ └────┘ ┴ ┴
typ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └────┘
67
68 lemma integrable_iff_norm (f : α → β) : integrable f ↔ (∫⁻ a, ennreal.of_real ∥f a∥) < ⊤ :=
id ┴ ┴ └────────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ ┴
src └────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ ┴
doc └────────┘ └┘ ┴ └─────────────┘
69 have eq : (λa, ennreal.of_real ∥f a∥) = (λa, (nnnorm(f a) : ennreal)),
id ┴ └─────────────┘ ┴┴ ┴┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └─────────────┘ ┴ ┴ ┴ └────┘ └─────┘
typ ┴ └─────────────┘ ┴┴ ┴┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └─────────────┘ └────┘ └─────┘
70 by { funext, rw of_real_norm_eq_coe_nnnorm },
id └────────────────────────┘
src └────┘ └─┘└────────────────────────┘┴
typ └────┘ └─┘└────────────────────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ ┴
st └───────┘└──────────────────────────────┘└┘
71 iff.intro (by { rw eq, exact λh, h }) $ by { rw eq, exact λh, h }
id └───────┘ └┘ └┘
src └───────┘ └─┘└┘ └────┘ └─┘ ┴ └─┘└┘ └────┘ └─┘ ┴
typ └───────┘ └─┘└┘ └────┘ └─┘ ┴ └─┘└┘ └────┘ └─┘ ┴
doc └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
txt └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
par └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
pid ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
st └──────┘└────────────┘└┘ └──────┘└────────────┘└┘
72
73 lemma integrable_iff_edist (f : α → β) : integrable f ↔ (∫⁻ a, edist (f a) 0) < ⊤ :=
id ┴ ┴ └────────┘ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ └┘ ┴ └───┘ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └────────┘ └┘ ┴
74 have eq : (λa, edist (f a) 0) = (λa, (nnnorm(f a) : ennreal)),
id ┴ └───┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └───┘ ┴ └────┘ └─────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └────┘ └─────┘
75 by { funext, rw edist_eq_coe_nnnorm },
id └─────────────────┘
src └────┘ └─┘└─────────────────┘┴
typ └────┘ └─┘└─────────────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ ┴
st └───────┘└───────────────────────┘└┘
76 iff.intro (by { rw eq, exact λh, h }) $ by { rw eq, exact λh, h }
id └───────┘ └┘ └┘
src └───────┘ └─┘└┘ └────┘ └─┘ ┴ └─┘└┘ └────┘ └─┘ ┴
typ └───────┘ └─┘└┘ └────┘ └─┘ ┴ └─┘└┘ └────┘ └─┘ ┴
doc └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
txt └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
par └─┘ └────┘ └─┘ ┴ └─┘ └────┘ └─┘ ┴
pid ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
st └──────┘└────────────┘└┘ └──────┘└────────────┘└┘
77
78 lemma integrable_iff_of_real {f : α → ℝ} (h : ∀ₘ a, 0 ≤ f a) :
id ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └┘ ┴
79 integrable f ↔ (∫⁻ a, ennreal.of_real (f a)) < ⊤ :=
id └────────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴
typ └────────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └┘ ┴ └─────────────┘
80 have lintegral_eq : (∫⁻ a, ennreal.of_real ∥f a∥) = (∫⁻ a, ennreal.of_real (f a)) :=
id └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └┘ ┴┴ └─────────────┘ ┴ ┴
src └┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘ ┴ └─────────────┘
typ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └┘ ┴┴ └─────────────┘ ┴ ┴
doc └┘ ┴ └─────────────┘ └┘ ┴ └─────────────┘
81 begin
st └─────
82 apply lintegral_congr_ae,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
83 filter_upwards [h],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ───────────────────┘└─
84 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
85 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
86 rw [real.norm_eq_abs, abs_of_nonneg],
id └──────────────┘ └───────────┘
src └──┘└──────────────┘└┘└───────────┘┴
typ └──┘└──────────────┘└┘└───────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────┘└─────────────┘└──
87 exact h
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘
88 end,
st └─┘
89 by rw [integrable_iff_norm, lintegral_eq]
id └─────────────────┘ └──────────┘
src └──┘└─────────────────┘└┘ └─
typ └──┘└─────────────────┘└┘└──────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────┘└────────────┘┴└
90
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
91 lemma integrable_of_ae_eq {f g : α → β} (hf : integrable f) (h : ∀ₘ a, f a = g a) : integrable g :=
id ┴ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └┘ ┴ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └┘ ┴ └────────┘
92 begin
st └─────
93 simp only [integrable] at *,
id └────────┘
src └─────────┘└────────┘└────┘
typ └─────────┘└────────┘└────┘
doc └─────────┘└────────┘└────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ────────────────────────────┘└─
94 have : (∫⁻ (a : α), ↑(nnnorm (f a))) = (∫⁻ (a : α), ↑(nnnorm (g a))),
id ┴ ┴ ┴ └┘ ┴ ┴ └────┘ ┴
src └─────┘ └────┘ ┴ ┴┴ ┴ ┴ └──┘┴┴ └┘└────┘ ┴┴┴ └────┘┴ ┴ └─┘
typ └─────┘ └────┘ ┴ ┴┴ ┴ ┴┴ └──┘┴┴ └┘└────┘┴┴┴┴ └────┘┴ ┴┴ └─┘
doc └─────┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘└────┘ ┴┴┴ └────┘┴ ┴ └─┘
txt └─────┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘
par └─────┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘
pid └───┘└┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────┘└─
95 { apply lintegral_congr_ae,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└──────────────────────┘└─
96 filter_upwards [h],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ─────────────────────┘└─
97 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
98 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────────────────┘└─
99 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
100 rw h },
id ┴
src └─┘ ┴
typ └─┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ────────┘└┘└
101 rwa ← this
id └──┘
src └────┘ ┴
typ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └─┘ ┴
st ────────────┘
102 end
st └─┘
103
104 lemma integrable_congr_ae {f g : α → β} (h : ∀ₘ a, f a = g a) : integrable f ↔ integrable g :=
id ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴
src └┘ ┴ ┴ └────────┘ ┴ └────────┘
typ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴
doc └┘ ┴ └────────┘ └────────┘
st ┴
105 iff.intro (λhf, integrable_of_ae_eq hf h) (λhg, integrable_of_ae_eq hg (all_ae_eq_symm h))
id └───────┘ └┘ └─────────────────┘ └┘ ┴ └┘ └─────────────────┘ └┘ └────────────┘ ┴
src └───────┘ └─────────────────┘ └─────────────────┘ └────────────┘
typ └───────┘ └┘ └─────────────────┘ └┘ ┴ └┘ └─────────────────┘ └┘ └────────────┘ ┴
st ┴
106
107 lemma integrable_of_le_ae {f : α → β} {g : α → γ} (h : ∀ₘ a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
id ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴
src └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴
doc └┘ ┴ └────────┘
108 integrable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
109 begin
st └─────
110 simp only [integrable_iff_norm] at *,
id └─────────────────┘
src └─────────┘└─────────────────┘└────┘
typ └─────────┘└─────────────────┘└────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ─────────────────────────────────────┘└─
111 calc (∫⁻ a, ennreal.of_real ∥f a∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥g a∥) :
id └──┘ └┘ ┴┴ ┴┴ ┴ ┴ └─────────────┘ ┴
src └──┘ └┘ ┴ ┴ ┴ └─────────────┘
typ └──┘ └┘ ┴┴ ┴┴ ┴ ┴ └─────────────┘ ┴
doc └──┘ └┘ ┴ └─────────────┘
st ─────────────────────────────────────────────────────────────────────────────
112 lintegral_le_lintegral_ae (by { filter_upwards [h], assume a h, exact of_real_le_of_real h })
id └───────────────────────┘ └────────────────┘ ┴
src └───────────────────────┘ └──────────────┘ ┴ └────────┘ └────┘└────────────────┘┴ ┴
typ └───────────────────────┘ └──────────────┘ ┴ └────────┘ └────┘└────────────────┘┴┴┴
doc └──────────────┘ ┴ └────────┘ └────┘ ┴ ┴
txt └──────────────┘ ┴ └────────┘ └────┘ ┴ ┴
par └──────────────┘ ┴ └────────┘ └────┘ ┴ ┴
pid └┘ ┴ └────────┘ ┴ ┴ ┴
st ────────────────────────────────┘└───────────────────┘└──────────┘└───────────────────────────┘└┘└
113 ... < ⊤ : hg
id ┴ └┘
src ┴
typ ┴ └┘
st ───────────────┘└
114 end
st ──┘
115
116 lemma integrable_of_le {f : α → β} {g : α → γ} (h : ∀a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴
doc └────────┘
117 integrable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
118 integrable_of_le_ae (univ_mem_sets' h) hg
id └─────────────────┘ └────────────┘ ┴ └┘
src └─────────────────┘ └────────────┘
typ └─────────────────┘ └────────────┘ ┴ └┘
119
120 lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) :
id ┴ ┴
typ ┴ ┴
121 (∫⁻ a, nnnorm (f a)) = ∫⁻ a, edist (f a) 0 :=
id └┘ ┴┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴
src └┘ ┴ └────┘ ┴ └┘ ┴ └───┘
typ └┘ ┴┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴
doc └┘ ┴ └────┘ └┘ ┴
122 by { congr, funext, rw edist_eq_coe_nnnorm }
id └─────────────────┘
src └───┘ └────┘ └─┘└─────────────────┘┴
typ └───┘ └────┘ └─┘└─────────────────┘┴
doc └────┘ └─┘ ┴
txt └───┘ └────┘ └─┘ ┴
par └───┘ └────┘ └─┘ ┴
pid ┴ ┴
st └──────┘└──────┘└───────────────────────┘└┘
123
124 lemma lintegral_norm_eq_lintegral_edist (f : α → β) :
id ┴ ┴
typ ┴ ┴
125 (∫⁻ a, ennreal.of_real ∥f a∥) = ∫⁻ a, edist (f a) 0 :=
id └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └┘ ┴┴ └───┘ ┴ ┴
src └┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘ ┴ └───┘
typ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └┘ ┴┴ └───┘ ┴ ┴
doc └┘ ┴ └─────────────┘ └┘ ┴
126 by { congr, funext, rw [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm] }
id └────────────────────────┘ └─────────────────┘
src └───┘ └────┘ └──┘└────────────────────────┘└┘└─────────────────┘└┘
typ └───┘ └────┘ └──┘└────────────────────────┘└┘└─────────────────┘└┘
doc └────┘ └──┘ └┘ └┘
txt └───┘ └────┘ └──┘ └┘ └┘
par └───┘ └────┘ └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └──────┘└──────┘└──────────────────────────────┘└───────────────────┘┴┴└┘
127
128 lemma lintegral_edist_triangle [second_countable_topology β] {f g h : α → β}
id └───────────────────────┘ ┴ ┴ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴ ┴ ┴
doc └───────────────────────┘
129 (hf : measurable f) (hg : measurable g) (hh : measurable h) :
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘
130 (∫⁻ a, edist (f a) (g a)) ≤ (∫⁻ a, edist (f a) (h a)) + ∫⁻ a, edist (g a) (h a) :=
id └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └┘ ┴ └───┘
typ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └┘ ┴ └┘ ┴
131 begin
st └─────
132 rw ← lintegral_add (measurable.edist hf hh) (measurable.edist hg hh),
id └───────────┘ └┘ └──────────────┘ └┘ └┘
src └───┘└───────────┘┴ ┴ ┴ └┘ └──────────────┘┴ ┴ ┴
typ └───┘└───────────┘┴ ┴└┘┴ └┘ └──────────────┘┴└┘┴└┘┴
doc └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
133 apply lintegral_le_lintegral,
id └────────────────────┘
src └────┘└────────────────────┘
typ └────┘└────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
134 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
135 have := edist_triangle (f a) (h a) (g a),
id └────────────┘ ┴ ┴ ┴ ┴
src └──────┘└────────────┘┴ ┴ └┘ ┴ └┘ ┴ ┴
typ └──────┘└────────────┘┴ ┴┴ └┘ ┴┴ └┘ ┴┴┴┴
doc └──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
txt └──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
par └──────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
pid └───┘└─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────┘└─
136 convert this,
id └──┘
src └──────┘
typ └──────┘└──┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────────┘└─
137 rw edist_comm (h a) (g a),
id └────────┘ ┴ ┴ ┴
src └─┘└────────┘┴ ┴ └┘ ┴ ┴
typ └─┘└────────┘┴ ┴┴ └┘ ┴┴┴┴
doc └─┘ ┴ ┴ └┘ ┴ ┴
txt └─┘ ┴ ┴ └┘ ┴ ┴
par └─┘ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴
st ──────────────────────────┘└─
138 end
st ──┘
139
140 lemma lintegral_edist_lt_top [second_countable_topology β] {f g : α → β}
id └───────────────────────┘ ┴ ┴ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴ ┴ ┴
doc └───────────────────────┘
141 (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘ └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘ └────────┘
142 (∫⁻ a, edist (f a) (g a)) < ⊤ :=
id └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ ┴ ┴
typ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴
143 lt_of_le_of_lt
id └────────────┘
src └────────────┘
typ └────────────┘
144 (lintegral_edist_triangle hfm hgm (measurable_const : measurable (λa, (0 : β))))
id └──────────────────────┘ └─┘ └─┘ └──────────────┘ └────────┘ ┴ ┴
src └──────────────────────┘ └──────────────┘ └────────┘
typ └──────────────────────┘ └─┘ └─┘ └──────────────┘ └────────┘ ┴ ┴
doc └────────┘
145 (ennreal.add_lt_top.2 $ by { split; rw ← integrable_iff_edist; assumption })
id └────────────────┘┴ └──────────────────┘
src └────────────────┘┴ └───┘ └───┘└──────────────────┘ └─────────┘
typ └────────────────┘┴ └───┘ └───┘└──────────────────┘ └─────────┘
doc └───┘ └───┘ └─────────┘
txt └───┘ └───┘ └─────────┘
par └───┘ └───┘ └─────────┘
pid └─┘ ┴
st └──────────────────────────────────────────────┘└┘
146
147 @[simp] lemma lintegral_nnnorm_zero : (∫⁻ a : α, nnnorm (0 : β)) = 0 := by simp
id └┘ ┴┴ └────┘ ┴ ┴
src └┘ ┴ └────┘ ┴ └────
typ └┘ ┴┴ └────┘ ┴ ┴ └────
doc └──┘ └┘ ┴ └────┘ └────
txt └────
par └────
pid └
st └─────
148
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
149 variables (α β)
150 @[simp] lemma integrable_zero : integrable (λa:α, (0:β)) :=
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
doc └──┘ └────────┘
151 by { have := coe_lt_top, simpa [integrable] }
id └────────┘ └────────┘
src └──────┘└────────┘ └─────┘└────────┘└┘
typ └──────┘└────────┘ └─────┘└────────┘└┘
doc └──────┘ └─────┘└────────┘└┘
txt └──────┘ └─────┘ └┘
par └──────┘ └─────┘ └┘
pid └───┘└─┘ ┴┴ ┴┴
st └───────────────────┘└───────────────────┘└┘
152 variables {α β}
153
154 lemma lintegral_nnnorm_add {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
155 (∫⁻ a, nnnorm (f a) + nnnorm (g a)) = (∫⁻ a, nnnorm (f a)) + ∫⁻ a, nnnorm (g a) :=
id └┘ ┴┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴
src └┘ ┴ └────┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘
typ └┘ ┴┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴
doc └┘ ┴ └────┘ └────┘ └┘ ┴ └────┘ └┘ ┴ └────┘
156 lintegral_add (measurable.coe_nnnorm hf) (measurable.coe_nnnorm hg)
id └───────────┘ └───────────────────┘ └┘ └───────────────────┘ └┘
src └───────────┘ └───────────────────┘ └───────────────────┘
typ └───────────┘ └───────────────────┘ └┘ └───────────────────┘ └┘
157
158 lemma integrable.add {f g : α → β} (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘ └────────┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘
159 (hgi : integrable g): integrable (λa, f a + g a) :=
id └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
160 calc
161 (∫⁻ (a : α), ↑(nnnorm ((f + g) a))) ≤ ∫⁻ (a : α), ↑(nnnorm (f a)) + ↑(nnnorm (g a)) :
id └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └┘ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ └────┘ ┴ ┴ └────┘
typ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └┘ ┴ └────┘ └┘ ┴ └────┘ └────┘
162 lintegral_le_lintegral _ _
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
163 (assume a, by { simp only [coe_add.symm, coe_le_coe], exact nnnorm_add_le _ _ })
id ┴ └────────┘ └───────────┘
src └─────────┘ └┘└────────┘┴ └────┘└───────────┘└───┘
typ ┴ └─────────┘└──────────┘└┘└────────┘┴ └────┘└───────────┘└───┘
doc └─────────┘ └┘ ┴ └────┘ └───┘
txt └─────────┘ └┘ ┴ └────┘ └───┘
par └─────────┘ └┘ ┴ └────┘ └───┘
pid ┴└──┘└┘ └┘ ┴ ┴ └──┘┴
st └─────────────────────────────────────┘└────────────────────────┘└┘
164 ... = _ :
165 lintegral_nnnorm_add hfm hgm
id └──────────────────┘ └─┘ └─┘
src └──────────────────┘
typ └──────────────────┘ └─┘ └─┘
166 ... < ⊤ : add_lt_top.2 ⟨hfi, hgi⟩
id ┴ └────────┘┴ └─┘ └─┘
src ┴ └────────┘┴
typ ┴ └────────┘┴ └─┘ └─┘
167
168 lemma integrable_finset_sum {ι} [second_countable_topology β] (s : finset ι) {f : ι → α → β}
id └───────────────────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └───────────────────────┘ └────┘
typ └───────────────────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └───────────────────────┘ └────┘
169 (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i)) :
id ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘ └────────┘
170 integrable (λ a, s.sum (λ i, f i a)) :=
id └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └────────┘ └──┘
typ └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └────────┘
171 begin
st └─────
172 refine finset.induction_on s _ _,
id └─────────────────┘ ┴
src └─────┘└─────────────────┘┴ └──┘
typ └─────┘└─────────────────┘┴┴└──┘
doc └─────┘└─────────────────┘┴ └──┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ─────────────────────────────────┘└─
173 { simp only [finset.sum_empty, integrable_zero] },
id └──────────────┘ └─────────────┘
src └─────────┘└──────────────┘└┘└─────────────┘└┘
typ └─────────┘└──────────────┘└┘└─────────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ───┘└────────────────────────────────────────────┘└┘└
174 { assume i s his ih,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └───────────────┘
st ────────────────────┘└─
175 simp only [his, finset.sum_insert, not_false_iff],
id └─┘ └───────────────┘ └───────────┘
src └─────────┘ └┘└───────────────┘└┘└───────────┘┴
typ └─────────┘└─┘└┘└───────────────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────┘└─
176 refine (hfi _).add (hfm _) (measurable_finset_sum s hfm) ih }
id └─┘ └───────────────────┘ ┴ └─┘ └┘
src └─────┘ └──────┘ └──┘ └───────────────────┘┴ ┴ └┘ ┴
typ └─────┘ └─┘└──────┘ └──┘ └───────────────────┘┴┴┴└─┘└┘└┘┴
doc └─────┘ └──────┘ └──┘ ┴ ┴ └┘ ┴
txt └─────┘ └──────┘ └──┘ ┴ ┴ └┘ ┴
par └─────┘ └──────┘ └──┘ ┴ ┴ └┘ ┴
pid ┴ └──────┘ └──┘ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
177 end
st ──┘
178
179 lemma lintegral_nnnorm_neg {f : α → β} :
id ┴ ┴
typ ┴ ┴
180 (∫⁻ (a : α), ↑(nnnorm ((-f) a))) = ∫⁻ (a : α), ↑(nnnorm ((f) a)) :=
id └┘ ┴ ┴ ┴ └────┘ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └┘ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └────┘
typ └┘ ┴ ┴ ┴ └────┘ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └┘ ┴ └────┘ └┘ ┴ └────┘
181 lintegral_congr_ae $ by { filter_upwards [], simp }
id └────────────────┘
src └────────────────┘ └───────────────┘ └───┘
typ └────────────────┘ └───────────────┘ └───┘
doc └───────────────┘ └───┘
txt └───────────────┘ └───┘
par └───────────────┘ └───┘
pid └─┘ ┴
st └──────────────────┘└─────┘└┘
182
183 lemma integrable.neg {f : α → β} : integrable f → integrable (λa, -f a) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴
src └────────┘ └────────┘ ┴
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴
doc └────────┘ └────────┘
184 assume hfi, calc _ = _ : lintegral_nnnorm_neg
id └─┘ └──────────────────┘
src └──────────────────┘
typ └─┘ └──────────────────┘
185 ... < ⊤ : hfi
id ┴ └─┘
src ┴
typ ┴ └─┘
186
187 @[simp] lemma integrable_neg_iff (f : α → β) : integrable (λa, -f a) ↔ integrable f :=
id ┴ ┴ └────────┘ ┴ ┴┴ ┴ ┴ └────────┘ ┴
src └────────┘ ┴ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ ┴┴ ┴ ┴ └────────┘ ┴
doc └──┘ └────────┘ └────────┘
188 begin
st └─────
189 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
190 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
191 simpa only [_root_.neg_neg] using h.neg },
id └────────────┘ └───┘
src └──────────┘└────────────┘└──────┘└───┘┴
typ └──────────┘└────────────┘└──────┘└───┘┴
doc └──────────┘ └──────┘ ┴
txt └──────────┘ └──────┘ ┴
par └──────────┘ └──────┘ ┴
pid ┴└──┘└┘ ┴┴└────┘ ┴
st ───────────────────────────────────────────┘└┘└
192 exact integrable.neg
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────┘
193 end
st └─┘
194
195 lemma integrable.sub {f g : α → β} (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘ └────────┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘
196 (hgi : integrable g) : integrable (λa, f a - g a) :=
id └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
197 by { simp only [sub_eq_add_neg], exact hfi.add hfm (measurable.neg hgm) (integrable.neg hgi) }
id └────────────┘ └─────┘ └─┘ └────────────┘ └─┘ └────────────┘ └─┘
src └─────────┘└────────────┘┴ └────┘└─────┘┴ ┴ └────────────┘┴ └┘ └────────────┘┴ └┘
typ └─────────┘└────────────┘┴ └────┘└─────┘┴└─┘┴ └────────────┘┴└─┘└┘ └────────────┘┴└─┘└┘
doc └─────────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
txt └─────────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └─────────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid ┴└──┘└┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴
st └───────────────────────────┘└────────────────────────────────────────────────────────────┘└┘
198
199 lemma integrable.norm {f : α → β} (hfi : integrable f) : integrable (λa, ∥f a∥) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴┴
src └────────┘ └────────┘ ┴ ┴
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴┴
doc └────────┘ └────────┘
200 have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal),
id ┴ └────┘ ┴┴ ┴┴ └─────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └────┘ ┴ ┴ └─────┘ ┴ └────┘ └─────┘
typ ┴ └────┘ ┴┴ ┴┴ └─────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └────┘ └─────┘ └────┘ └─────┘
201 by { funext, rw nnnorm_norm },
id └─────────┘
src └────┘ └─┘└─────────┘┴
typ └────┘ └─┘└─────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ ┴
st └───────┘└───────────────┘└┘
202 by { rwa [integrable, eq] }
id └────────┘ └┘
src └───┘└────────┘└┘└┘└┘
typ └───┘└────────┘└┘└┘└┘
doc └───┘└────────┘└┘ └┘
txt └───┘ └┘ └┘
par └───┘ └┘ └┘
pid └┘ └┘ ┴┴
st └────────────────┘└──┘┴┴└┘
203
204 lemma integrable_norm_iff (f : α → β) : integrable (λa, ∥f a∥) ↔ integrable f :=
id ┴ ┴ └────────┘ ┴ ┴┴ ┴┴ ┴ └────────┘ ┴
src └────────┘ ┴ ┴ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ ┴┴ ┴┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
205 have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal),
id ┴ └────┘ ┴┴ ┴┴ └─────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └────┘ ┴ ┴ └─────┘ ┴ └────┘ └─────┘
typ ┴ └────┘ ┴┴ ┴┴ └─────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └────┘ └─────┘ └────┘ └─────┘
206 by { funext, rw nnnorm_norm },
id └─────────┘
src └────┘ └─┘└─────────┘┴
typ └────┘ └─┘└─────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ ┴
st └───────┘└───────────────┘└┘
207 by { rw [integrable, integrable, eq] }
id └────────┘ └────────┘ └┘
src └──┘└────────┘└┘└────────┘└┘└┘└┘
typ └──┘└────────┘└┘└────────┘└┘└┘└┘
doc └──┘└────────┘└┘└────────┘└┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └───────────────┘└──────────┘└──┘┴┴└┘
208
209 lemma integrable_of_integrable_bound {f : α → β} {bound : α → ℝ} (h : integrable bound)
id ┴ ┴ ┴ ┴ └────────┘ └───┘
src ┴ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ └───┘
doc └────────┘
210 (h_bound : ∀ₘ a, ∥f a∥ ≤ bound a) : integrable f :=
id └┘ ┴┴ ┴┴ ┴┴ ┴ └───┘ ┴ └────────┘ ┴
src └┘ ┴ ┴ ┴ ┴ └────────┘
typ └┘ ┴┴ ┴┴ ┴┴ ┴ └───┘ ┴ └────────┘ ┴
doc └┘ ┴ └────────┘
211 have h₁ : ∀ₘ a, (nnnorm (f a) : ennreal) ≤ ennreal.of_real (bound a),
id └┘ ┴┴ └────┘ ┴ ┴ └─────┘ ┴ └─────────────┘ └───┘ ┴
src └┘ ┴ └────┘ └─────┘ ┴ └─────────────┘
typ └┘ ┴┴ └────┘ ┴ ┴ └─────┘ ┴ └─────────────┘ └───┘ ┴
doc └┘ ┴ └────┘ └─────┘ └─────────────┘
212 begin
st └─────
213 filter_upwards [h_bound],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ─────────────────────────┘└─
214 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
215 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
216 calc (nnnorm (f a) : ennreal) = ennreal.of_real (∥f a∥) : by rw of_real_norm_eq_coe_nnnorm
id └──┘ └────┘ └─────┘ ┴┴ ┴ └────────────────────────┘
src └──┘ └────┘ └─────┘ ┴ ┴ └─┘└────────────────────────┘└
typ └──┘ └────┘ └─────┘ ┴┴ ┴ └─┘└────────────────────────┘└
doc └──┘ └────┘ └─────┘ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ─────────────────────────────────────────────────────────────┘└──────────────────────────────
217 ... ≤ ennreal.of_real (bound a) : ennreal.of_real_le_of_real h
id └─────────────┘ └───┘ ┴ └────────────────────────┘ ┴
src ───┘ └─────────────┘ └────────────────────────┘
typ ───┘ └─────────────┘ └───┘ ┴ └────────────────────────┘ ┴
doc ───┘ └─────────────┘
txt ───┘
par ───┘
pid ───┘
st ───┘└────────────────────────────────────────────────────────────┘└
218 end,
st ──┘
219 calc (∫⁻ a, nnnorm (f a)) ≤ (∫⁻ a, ennreal.of_real (bound a)) :
id └┘ ┴┴ └────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ └───┘ ┴
src └┘ ┴ └────┘ └┘ ┴ └─────────────┘
typ └┘ ┴┴ └────┘ ┴ ┴ └┘ ┴┴ └─────────────┘ └───┘ ┴
doc └┘ ┴ └────┘ └┘ ┴ └─────────────┘
220 by { apply lintegral_le_lintegral_ae, exact h₁ }
id └───────────────────────┘ └┘
src └────┘└───────────────────────┘ └────┘ ┴
typ └────┘└───────────────────────┘ └────┘└┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st └────────────────────────────────┘└─────────┘└┘
221 ... ≤ (∫⁻ a, ennreal.of_real ∥bound a∥) : lintegral_le_lintegral _ _ $
id └┘ ┴┴ └─────────────┘ ┴└───┘ ┴┴ └────────────────────┘
src └┘ ┴ └─────────────┘ ┴ ┴ └────────────────────┘
typ └┘ ┴┴ └─────────────┘ ┴└───┘ ┴┴ └────────────────────┘
doc └┘ ┴ └─────────────┘
222 by { assume a, apply ennreal.of_real_le_of_real, exact le_max_left (bound a) (-bound a) }
id └────────────────────────┘ └─────────┘ ┴└───┘ ┴
src └──────┘ └────┘└────────────────────────┘ └────┘└─────────┘┴ ┴ └┘ ┴ ┴ └┘
typ └──────┘ └────┘└────────────────────────┘ └────┘└─────────┘┴ ┴ └┘ ┴└───┘┴┴└┘
doc └──────┘ └────┘ └────┘ ┴ ┴ └┘ ┴ └┘
txt └──────┘ └────┘ └────┘ ┴ ┴ └┘ ┴ └┘
par └──────┘ └────┘ └────┘ ┴ ┴ └┘ ┴ └┘
pid └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴
st └─────────┘└────────────────────────────────┘└───────────────────────────────────────┘└┘
223 ... < ⊤ : by { rwa [integrable_iff_norm] at h }
id ┴ └─────────────────┘
src ┴ └───┘└─────────────────┘└─────┘
typ ┴ └───┘└─────────────────┘└─────┘
doc └───┘ └─────┘
txt └───┘ └─────┘
par └───┘ └─────┘
pid └┘ ┴└───┘┴
st └─────────────────────────┘┴└────┘└┘
224
225 section dominated_convergence
226
227 variables {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id ┴ ┴
src ┴ ┴
typ ┴ ┴
228
229 lemma all_ae_of_real_F_le_bound (h : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a) :
id ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
doc └┘ ┴
230 ∀ n, ∀ₘ a, ennreal.of_real ∥F n a∥ ≤ ennreal.of_real (bound a) :=
id ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴┴ ┴ └─────────────┘ └───┘ ┴
src └┘ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘
typ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴┴ ┴ └─────────────┘ └───┘ ┴
doc └┘ ┴ └─────────────┘ └─────────────┘
231 λn, by filter_upwards [h n] λ a h, ennreal.of_real_le_of_real h
id ┴ ┴ ┴ └────────────────────────┘
src └──────────────┘ ┴ └┘ └────┘└────────────────────────┘┴ └
typ ┴ └──────────────┘┴┴┴└┘ └────┘└────────────────────────┘┴ └
doc └──────────────┘ ┴ └┘ └────┘ ┴ └
txt └──────────────┘ ┴ └┘ └────┘ ┴ └
par └──────────────┘ ┴ └┘ └────┘ ┴ └
pid └┘ ┴ ┴┴ └────┘ ┴ └
st └─────────────────────────────────────────────────────────
232
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
233 lemma all_ae_tendsto_of_real_norm (h : ∀ₘ a, tendsto (λ n, F n a) at_top $ 𝓝 $ f a) :
id └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └─────┘ └────┘ ┴
typ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └┘ ┴ └─────┘ └────┘ ┴
234 ∀ₘ a, tendsto (λn, ennreal.of_real ∥F n a∥) at_top $ 𝓝 $ ennreal.of_real ∥f a∥ :=
id └┘ ┴┴ └─────┘ ┴ └─────────────┘ ┴┴ ┴ ┴┴ └────┘ ┴ └─────────────┘ ┴┴ ┴┴
src └┘ ┴ └─────┘ └─────────────┘ ┴ ┴ └────┘ ┴ └─────────────┘ ┴ ┴
typ └┘ ┴┴ └─────┘ ┴ └─────────────┘ ┴┴ ┴ ┴┴ └────┘ ┴ └─────────────┘ ┴┴ ┴┴
doc └┘ ┴ └─────┘ └─────────────┘ └────┘ ┴ └─────────────┘
235 by filter_upwards [h]
src └──────────────┘ └─
typ └──────────────┘ └─
doc └──────────────┘ └─
txt └──────────────┘ └─
par └──────────────┘ └─
pid └┘ ┴└
st └───────────────────
236 λ a h, tendsto_of_real $ tendsto.comp (continuous.tendsto continuous_norm _) h
id └─────────────┘ └──────────┘ └────────────────┘ └─────────────┘
src ─┘ └────┘└─────────────┘┴ ┴└──────────┘┴ └────────────────┘┴└─────────────┘└──┘ └
typ ─┘ └────┘└─────────────┘┴ ┴└──────────┘┴ └────────────────┘┴└─────────────┘└──┘ └
doc ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ └
txt ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ └
par ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ └
pid ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────────────────────────────────
237
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
238 lemma all_ae_of_real_f_le_bound (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
doc └┘ ┴
239 (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └─────┘ └────┘ ┴
typ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └┘ ┴ └─────┘ └────┘ ┴
240 ∀ₘ a, ennreal.of_real ∥f a∥ ≤ ennreal.of_real (bound a) :=
id └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └─────────────┘ └───┘ ┴
src └┘ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘
typ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴ ┴ └─────────────┘ └───┘ ┴
doc └┘ ┴ └─────────────┘ └─────────────┘
241 begin
st └─────
242 have F_le_bound := all_ae_of_real_F_le_bound h_bound,
id └───────────────────────┘ └─────┘
src └─────────────────┘└───────────────────────┘┴
typ └─────────────────┘└───────────────────────┘┴└─────┘
doc └─────────────────┘ ┴
txt └─────────────────┘ ┴
par └─────────────────┘ ┴
pid └─────────────┘┴└─┘ ┴
st ─────────────────────────────────────────────────────┘└─
243 rw ← all_ae_all_iff at F_le_bound,
id └────────────┘
src └───┘└────────────┘└────────────┘
typ └───┘└────────────┘└────────────┘
doc └───┘ └────────────┘
txt └───┘ └────────────┘
par └───┘ └────────────┘
pid └─┘ └────────────┘
st ──────────────────────────────────┘└─
244 filter_upwards [all_ae_tendsto_of_real_norm h_lim, F_le_bound],
id └─────────────────────────┘ └───┘
src └──────────────┘└─────────────────────────┘┴ └┘ ┴
typ └──────────────┘└─────────────────────────┘┴└───┘└┘ ┴
doc └──────────────┘ ┴ └┘ ┴
txt └──────────────┘ ┴ └┘ ┴
par └──────────────┘ ┴ └┘ ┴
pid └┘ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
245 assume a tendsto_norm F_le_bound,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └──────────────────────────────┘
st ─────────────────────────────────┘└─
246 refine le_of_tendsto at_top_ne_bot tendsto_norm _,
id └───────────┘ └───────────┘ └──────────┘
src └─────┘└───────────┘┴└───────────┘┴ └┘
typ └─────┘└───────────┘┴└───────────┘┴└──────────┘└┘
doc └─────┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────┘└─
247 simp only [mem_at_top_sets, ge_iff_le, mem_set_of_eq, preimage_set_of_eq, nonempty_of_inhabited],
id └─────────────┘ └───────┘ └───────────┘ └────────────────┘ └───────────────────┘
src └─────────┘└─────────────┘└┘└───────┘└┘└───────────┘└┘└────────────────┘└┘└───────────────────┘┴
typ └─────────┘└─────────────┘└┘└───────┘└┘└───────────┘└┘└────────────────┘└┘└───────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248 use 0,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴┴
st ──────┘└─
249 assume n hn,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
250 exact F_le_bound n
id └────────┘ ┴
src └────┘ ┴ ┴
typ └────┘└────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────┘
251 end
st └─┘
252
253 lemma integrable_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
254 (bound_integrable : integrable bound)
id └────────┘ └───┘
src └────────┘
typ └────────┘ └───┘
doc └────────┘
255 (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
doc └┘ ┴
256 (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └─────┘ └────┘ ┴
typ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └┘ ┴ └─────┘ └────┘ ┴
257 integrable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
258 /- `∥F n a∥ ≤ bound a` and `∥F n a∥ --> ∥f a∥` implies `∥f a∥ ≤ bound a`,
259 and so `∫ ∥f∥ ≤ ∫ bound < ⊤` since `bound` is integrable -/
260 begin
st └─────
261 rw integrable_iff_norm,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
262 calc (∫⁻ a, (ennreal.of_real ∥f a∥)) ≤ ∫⁻ a, ennreal.of_real (bound a) :
id └──┘ └┘ ┴┴ ┴┴ ┴ ┴ └─────────────┘ └───┘
src └──┘ └┘ ┴ ┴ ┴ └─────────────┘
typ └──┘ └┘ ┴┴ ┴┴ ┴ ┴ └─────────────┘ └───┘
doc └──┘ └┘ ┴ └─────────────┘
st ───────────────────────────────────────────────────────────────────────────
263 lintegral_le_lintegral_ae $ all_ae_of_real_f_le_bound h_bound h_lim
id └───────────────────────┘ └───────────────────────┘ └─────┘ └───┘
src └───────────────────────┘ └───────────────────────┘
typ └───────────────────────┘ └───────────────────────┘ └─────┘ └───┘
st ────────────────────────────────────────────────────────────────────────
264 ... < ⊤ :
id ┴
src ┴
typ ┴
st ──────────────
265 begin
st ───┘└─────
266 rw ← integrable_iff_of_real,
id └────────────────────┘
src └───┘└────────────────────┘
typ └───┘└────────────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────────────────────┘└─
267 { exact bound_integrable },
id └──────────────┘
src └────┘ ┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└─────────────────────┘└┘└
268 filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h,
id └─────┘ └──────┘ └─────────┘
src └──────────────┘ └──┘ └────┘└──────┘┴ └─────────┘└──┘
typ └──────────────┘└─────┘└──┘ └────┘└──────┘┴ └─────────┘└──┘
doc └──────────────┘ └──┘ └────┘ ┴ └──┘
txt └──────────────┘ └──┘ └────┘ ┴ └──┘
par └──────────────┘ └──┘ └────┘ ┴ └──┘
pid └┘ └─┘┴ └────┘ ┴ └──┘
st ─────────────────────────────────────────────────────────────────┘└─
269 end
st ────────
270 end
st ──┘
271
272 lemma tendsto_lintegral_norm_of_dominated_convergence [second_countable_topology β]
id └───────────────────────┘ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴
doc └───────────────────────┘
273 {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
274 (F_measurable : ∀ n, measurable (F n))
id ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴
doc └────────┘
275 (f_measurable : measurable f)
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
276 (bound_integrable : integrable bound)
id └────────┘ └───┘
src └────────┘
typ └────────┘ └───┘
doc └────────┘
277 (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴
doc └┘ ┴
278 (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └─────┘ └────┘ ┴
typ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └┘ ┴ └─────┘ └────┘ ┴
279 tendsto (λn, ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0) :=
id └─────┘ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴
src └─────┘ └┘ ┴ └─────────────┘ ┴ ┴ ┴ └────┘ ┴
typ └─────┘ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴
doc └─────┘ └┘ ┴ └─────────────┘ └────┘ ┴
280 let b := λa, 2 * ennreal.of_real (bound a) in
id ┴ ┴ ┴ └─────────────┘ └───┘ ┴
src ┴ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ └───┘ ┴
doc └─────────────┘
281 /- `∥F n a∥ ≤ bound a` and `F n a --> f a` implies `∥f a∥ ≤ bound a`, and thus by the
282 triangle inequality, have `∥F n a - f a∥ ≤ 2 * (bound a). -/
283 have hb : ∀ n, ∀ₘ a, ennreal.of_real ∥F n a - f a∥ ≤ b a,
id ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └┘ ┴ └─────────────┘
284 begin
st └─────
285 assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
286 filter_upwards [all_ae_of_real_F_le_bound h_bound n, all_ae_of_real_f_le_bound h_bound h_lim],
id └───────────────────────┘ └─────┘ ┴ └───────────────────────┘ └─────┘ └───┘
src └──────────────┘└───────────────────────┘┴ ┴ └┘└───────────────────────┘┴ ┴ ┴
typ └──────────────┘└───────────────────────┘┴└─────┘┴┴└┘└───────────────────────┘┴└─────┘┴└───┘┴
doc └──────────────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid └┘ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
287 assume a h₁ h₂,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
288 calc ennreal.of_real ∥F n a - f a∥ ≤ (ennreal.of_real ∥F n a∥) + (ennreal.of_real ∥f a∥) :
id └──┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └─────────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────────────
289 begin
st ─┘└─────
290 rw [← ennreal.of_real_add],
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ────────────────────────────┘└──
291 apply of_real_le_of_real,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
292 { apply norm_sub_le }, { exact norm_nonneg _ }, { exact norm_nonneg _ }
id └─────────┘ └─────────┘ └─────────┘
src └────┘└─────────┘┴ └────┘└─────────┘└─┘ └────┘└─────────┘└─┘
typ └────┘└─────────┘┴ └────┘└─────────┘└─┘ └────┘└─────────┘└─┘
doc └────┘ ┴ └────┘ └─┘ └────┘ └─┘
txt └────┘ ┴ └────┘ └─┘ └────┘ └─┘
par └────┘ ┴ └────┘ └─┘ └────┘ └─┘
pid ┴ ┴ ┴ └┘┴ ┴ └┘┴
st ─────┘└────────────────┘└┘└─┘└──────────────────┘└┘└─────────────────────┘└─
293 end
st ────┘└
294 ... ≤ (ennreal.of_real (bound a)) + (ennreal.of_real (bound a)) : add_le_add' h₁ h₂
id ┴ └───┘ └─────────┘ └┘ └┘
src ┴ └─────────┘
typ ┴ └───┘ └─────────┘ └┘ └┘
st ────────────────────────────────────────────────────────────────────────────────────────
295 ... = b a : by rw ← two_mul
id ┴ └─────┘
src └───┘└─────┘┴
typ ┴ └───┘└─────┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ─────────────────┘└────────────┘
296 end,
st └─┘
297 /- On the other hand, `F n a --> f a` implies that `∥F n a - f a∥ --> 0` -/
298 have h : ∀ₘ a, tendsto (λ n, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0),
id └┘ ┴┴ └─────┘ ┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴
src └┘ ┴ └─────┘ └─────────────┘ ┴ ┴ ┴ └────┘ ┴
typ └┘ ┴┴ └─────┘ ┴ └─────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴
doc └┘ ┴ └─────┘ └─────────────┘ └────┘ ┴
299 begin
st └─────
300 suffices h : ∀ₘ a, tendsto (λ n, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 $ ennreal.of_real 0),
id └┘ ┴ └─────┘ ┴ ┴ └────┘ ┴ └─────────────┘
src └───────────┘└┘└┘┴┴└─────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴┴ ┴└─────────────┘└─┘
typ └───────────┘└┘└┘┴┴└─────┘┴ └──┘ ┴ ┴┴ ┴ ┴ ┴┴┴ └┘└────┘┴ ┴┴ ┴└─────────────┘└─┘
doc └───────────┘└┘└┘┴┴└─────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴┴ ┴└─────────────┘└─┘
txt └───────────┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
par └───────────┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
pid └────────┘└─┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
301 { rwa ennreal.of_real_zero at h },
id └──────────────────┘
src └──┘└──────────────────┘└────┘
typ └──┘└──────────────────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴ └───┘┴
st ───┘└────────────────────────────┘└┘└
302 filter_upwards [h_lim],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ───────────────────────┘└─
303 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
304 refine tendsto.comp (continuous.tendsto continuous_of_real _) _,
id └──────────┘ └────────────────┘ └────────────────┘
src └─────┘└──────────┘┴ └────────────────┘┴└────────────────┘└───┘
typ └─────┘└──────────┘┴ └────────────────┘┴└────────────────┘└───┘
doc └─────┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └───┘
st ────────────────────────────────────────────────────────────────┘└─
305 rw ← tendsto_iff_norm_tendsto_zero,
id └───────────────────────────┘
src └───┘└───────────────────────────┘
typ └───┘└───────────────────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────────────────────────────────┘└─
306 exact h
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘
307 end,
st └─┘
308 /- Therefore, by the dominated convergence theorem for nonnegative integration, have
309 ` ∫ ∥f a - F n a∥ --> 0 ` -/
310 begin
st └─────
311 suffices h : tendsto (λn, ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 (∫⁻ (a:α), 0)),
id └─────┘ └─────────────┘ ┴ ┴ └────┘ └┘ ┴ ┴
src └───────────┘└─────┘┴ └─┘ └┘ ┴└─────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴ └┘└──┘ ┴┴└──┘
typ └───────────┘└─────┘┴ └─┘ └┘ ┴└─────────────┘┴ ┴┴ ┴ ┴ ┴┴┴ └┘└────┘┴ ┴ └┘└──┘┴┴┴└──┘
doc └───────────┘└─────┘┴ └─┘ └┘ ┴└─────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴ └┘└──┘ ┴┴└──┘
txt └───────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └──┘
par └───────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └──┘
pid └────────┘└─┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
312 { rwa lintegral_zero at h },
id └────────────┘
src └──┘└────────────┘└────┘
typ └──┘└────────────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴ └───┘┴
st ───┘└──────────────────────┘└┘└
313 -- Using the dominated convergence theorem.
st ──────────────────────────────────────────────
314 refine tendsto_lintegral_of_dominated_convergence _ _ hb _ _,
id └────────────────────────────────────────┘ └┘
src └─────┘└────────────────────────────────────────┘└───┘ └──┘
typ └─────┘└────────────────────────────────────────┘└───┘└┘└──┘
doc └─────┘└────────────────────────────────────────┘└───┘ └──┘
txt └─────┘ └───┘ └──┘
par └─────┘ └───┘ └──┘
pid ┴ └───┘ └──┘
st ─────────────────────────────────────────────────────────────┘└─
315 -- Show `λa, ∥f a - F n a∥` is measurable for all `n`
st ────────────────────────────────────────────────────────
316 { exact λn, measurable.comp measurable_of_real (measurable.norm (measurable.sub (F_measurable n)
id └─────────────┘ └────────────────┘ └─────────────┘ └────────────┘ └──────────┘
src └────┘ └─┘└─────────────┘┴└────────────────┘┴ └─────────────┘┴ └────────────┘┴ ┴ └─
typ └────┘ └─┘└─────────────┘┴└────────────────┘┴ └─────────────┘┴ └────────────┘┴ └──────────┘┴ └─
doc └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─
txt └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─
par └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─
st ───┘└──────────────────────────────────────────────────────────────────────────────────────────────
317 f_measurable)) },
id └──────────┘
src ─────┘ └─┘
typ ─────┘└──────────┘└─┘
doc ─────┘ └─┘
txt ─────┘ └─┘
par ─────┘ └─┘
pid ─────┘ └┘┴
st ────────────────────┘└┘└
318 -- Show `2 * bound` is integrable
st ────────────────────────────────────
319 { rw integrable_iff_of_real at bound_integrable,
id └────────────────────┘
src └─┘└────────────────────┘└──────────────────┘
typ └─┘└────────────────────┘└──────────────────┘
doc └─┘ └──────────────────┘
txt └─┘ └──────────────────┘
par └─┘ └──────────────────┘
pid ┴ └──────────────────┘
st ───┘└───────────────────────────────────────────┘└─
320 { calc (∫⁻ a, b a) = 2 * (∫⁻ a, ennreal.of_real (bound a)) :
id └──┘ ┴ ┴ ┴ ┴ └─────────────┘ └───┘
src └──┘ ┴ └─────────────┘
typ └──┘ ┴ ┴ ┴ ┴ └─────────────┘ └───┘
doc └──┘ └─────────────┘
st ─────┘└──────────────────────────────────────────────────────────
321 by { rw lintegral_const_mul', exact coe_ne_top }
id └──────────────────┘ └────────┘
src └─┘└──────────────────┘ └────┘└────────┘┴
typ └─┘└──────────────────┘ └────┘└────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────────┘└────────────────────────┘└─────────────────┘└┘
322 ... < ⊤ : mul_lt_top (coe_lt_top) bound_integrable },
id ┴ └────────┘ └────────┘ └──────────────┘
src ┴ └────────┘ └────────┘
typ ┴ └────────┘ └────────┘ └──────────────┘
st └────────────────────────────────────────────────────────┘└─┘└
323 filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h },
id └─────┘ └──────┘ └─────────┘
src └──────────────┘ └──┘ └────┘└──────┘┴ └─────────┘└──┘ ┴
typ └──────────────┘└─────┘└──┘ └────┘└──────┘┴ └─────────┘└──┘ ┴
doc └──────────────┘ └──┘ └────┘ ┴ └──┘ ┴
txt └──────────────┘ └──┘ └────┘ ┴ └──┘ ┴
par └──────────────┘ └──┘ └────┘ ┴ └──┘ ┴
pid └┘ └─┘┴ └────┘ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────────────┘└┘└
324 -- Show `∥f a - F n a∥ --> 0`
st ────────────────────────────────
325 { exact h }
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────┘└─
326 end
st ──┘
327
328 end dominated_convergence
329
330 section pos_part
331 /-! Lemmas used for defining the positive part of a `L¹` function -/
332
333 lemma integrable.max_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, max (f a) 0) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └─┘ ┴ ┴
src ┴ └────────┘ └────────┘ └─┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └─┘ ┴ ┴
doc └────────┘ └────────┘
334 begin
st └─────
335 simp only [integrable_iff_norm] at *,
id └─────────────────┘
src └─────────┘└─────────────────┘└────┘
typ └─────────┘└─────────────────┘└────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ─────────────────────────────────────┘└─
336 calc (∫⁻ a, ennreal.of_real ∥max (f a) 0∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥f a∥) :
id └──┘ └┘ ┴┴ ┴└─┘ ┴ ┴ └─────────────┘ ┴
src └──┘ └┘ ┴ ┴└─┘ ┴ └─────────────┘
typ └──┘ └┘ ┴┴ ┴└─┘ ┴ ┴ └─────────────┘ ┴
doc └──┘ └┘ ┴ └─────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────
337 lintegral_le_lintegral _ _
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
st ───────────────────────────────
338 begin
st ───┘└─────
339 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
340 apply of_real_le_of_real,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
341 simp only [real.norm_eq_abs],
id └──────────────┘
src └─────────┘└──────────────┘┴
typ └─────────┘└──────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────────────┘└─
342 calc abs (max (f a) 0) = max (f a) 0 : by { rw abs_of_nonneg, apply le_max_right }
id └─┘ └───────────┘ └──────────┘
src └─┘ └─┘└───────────┘ └────┘└──────────┘┴
typ └─┘ └─┘└───────────┘ └────┘└──────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─────────────────┘└───────────────────┘└┘
343 ... ≤ abs (f a) : max_le (le_abs_self _) (abs_nonneg _)
id └─┘ ┴ ┴ └────┘ └─────────┘ └────────┘
src └─┘ └────┘ └─────────┘ └────────┘
typ └─┘ ┴ ┴ └────┘ └─────────┘ └────────┘
st └─────────────────────────────────────────────────────────────┘└
344 end
st ──────┘└
345 ... < ⊤ : hf
id ┴ └┘
src ┴
typ ┴ └┘
st ───────────────┘└
346 end
st ──┘
347
348 lemma integrable.min_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, min (f a) 0) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └─┘ ┴ ┴
src ┴ └────────┘ └────────┘ └─┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └─┘ ┴ ┴
doc └────────┘ └────────┘
349 begin
st └─────
350 have : (λa, min (f a) 0) = (λa, - max (-f a) 0),
id └─┘ ┴ └─┘ ┴┴
src └─────┘ └─┘└─┘┴ ┴ └───┘┴┴ └─┘ ┴└─┘┴ ┴ ┴ └──┘
typ └─────┘ └─┘└─┘┴ ┴ └───┘┴┴ └─┘ ┴└─┘┴ ┴┴┴ └──┘
doc └─────┘ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └──┘
txt └─────┘ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └──┘
par └─────┘ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └──┘
pid └───┘└┘ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────┘└─
351 { funext, rw [min_eq_neg_max_neg_neg, neg_zero] },
id └────────────────────┘ └──────┘
src └────┘ └──┘└────────────────────┘└┘└──────┘└┘
typ └────┘ └──┘└────────────────────┘└┘└──────┘└┘
doc └────┘ └──┘ └┘ └┘
txt └────┘ └──┘ └┘ └┘
par └────┘ └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───┘└────┘└──────────────────────────┘└────────┘┴┴└┘└
352 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
353 exact (integrable.max_zero hf.neg).neg,
id └─────────────────┘ └────┘
src └────┘ └─────────────────┘┴└────┘└───┘
typ └────┘ └─────────────────┘┴└────┘└───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └──┘┴
st ───────────────────────────────────────┘└─
354 end
st ──┘
355
356 end pos_part
357
358 section normed_space
359 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
360
361 lemma integrable.smul (c : 𝕜) {f : α → β} : integrable f → integrable (λa, c • f a) :=
id ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
362 begin
st └─────
363 simp only [integrable], assume hfi,
id └────────┘
src └─────────┘└────────┘┴ └────────┘
typ └─────────┘└────────┘┴ └────────┘
doc └─────────┘└────────┘┴ └────────┘
txt └─────────┘ ┴ └────────┘
par └─────────┘ ┴ └────────┘
pid ┴└──┘└┘ ┴ └────────┘
st ───────────────────────┘└──────────┘└─
364 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────
365 (∫⁻ (a : α), nnnorm ((c • f) a)) = (∫⁻ (a : α), (nnnorm c) * nnnorm (f a)) :
id └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src └┘ ┴ ┴ ┴ └────┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
doc └┘ ┴ └────┘
st ─────────────────────────────────────────────────────────────────────────────────
366 begin
st ───┘└─────
367 apply lintegral_congr_ae,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
368 filter_upwards [],
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─┘
st ──────────────────────┘└─
369 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
370 simp only [nnnorm_smul, set.mem_set_of_eq, pi.smul_apply, ennreal.coe_mul]
id └─────────┘ └───────────────┘ └───────────┘ └─────────────┘
src └─────────┘└─────────┘└┘└───────────────┘└┘└───────────┘└┘└─────────────┘└─
typ └─────────┘└─────────┘└┘└───────────────┘└┘└───────────┘└┘└─────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st ─────────────────────────────────────────────────────────────────────────────────
371 end
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘└
372 ... < ⊤ :
id ┴
src ┴
typ ┴
st ──────────────
373 begin
st ───┘└─────
374 rw lintegral_const_mul',
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────┘└─
375 apply mul_lt_top,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
376 { exact coe_lt_top },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└───────────────┘└┘└
377 { exact hfi },
id └─┘
src └────┘ ┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└────────┘└┘└
378 { simp only [ennreal.coe_ne_top, ne.def, not_false_iff] }
id └────────────────┘ └────┘ └───────────┘
src └─────────┘└────────────────┘└┘└────┘└┘└───────────┘└┘
typ └─────────┘└────────────────┘└┘└────┘└┘└───────────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────┘└─
379 end
st ────────
380 end
st ──┘
381
382 lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (λa, c • f a) ↔ integrable f :=
id ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src ┴ └────────┘ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
383 begin
st └─────
384 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
385 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
386 simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.smul c⁻¹ },
id └───────┘ └────────────┘ └┘ └──────┘ └────┘ ┴└┘
src └──────────┘└───────┘└┘└────────────┘┴ └┘└──────┘└──────┘└────┘┴ └┘┴
typ └──────────┘└───────┘└┘└────────────┘┴└┘└┘└──────┘└──────┘└────┘┴┴└┘┴
doc └──────────┘ └┘ ┴ └┘ └──────┘ ┴ ┴
txt └──────────┘ └┘ ┴ └┘ └──────┘ ┴ ┴
par └──────────┘ └┘ ┴ └┘ └──────┘ ┴ ┴
pid ┴└──┘└┘ └┘ ┴ └┘ ┴┴└────┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────┘└┘└
387 exact integrable.smul _
id └─────────────┘
src └────┘└─────────────┘└─┘
typ └────┘└─────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────────────┘
388 end
st └─┘
389
390 end normed_space
391
392 variables [second_countable_topology β]
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
393
394 namespace ae_eq_fun
395
396 /-- An almost everywhere equal function is `integrable` if it has a finite distance to the origin.
397 Should mean the same thing as the predicate `integrable` over functions. -/
398 def integrable (f : α →ₘ β) : Prop := f ∈ ball (0 : α →ₘ β) ⊤
id ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴
src └┘ ┴ └──┘ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴
doc └┘ └──┘ └┘
399
400 lemma integrable_mk (f : α → β) (hf : measurable f) :
id ┴ ┴ └────────┘ ┴
src └────────┘
typ ┴ ┴ └────────┘ ┴
doc └────────┘
401 (integrable (mk f hf)) ↔ measure_theory.integrable f :=
id └────────┘ └┘ ┴ └┘ ┴ └───────────────────────┘ ┴
src └────────┘ └┘ ┴ └───────────────────────┘
typ └────────┘ └┘ ┴ └┘ ┴ └───────────────────────┘ ┴
doc └────────┘ └┘ └───────────────────────┘
402 by simp [integrable, zero_def, edist_mk_mk', measure_theory.integrable, nndist_eq_nnnorm]
id └────────┘ └──────┘ └──────────┘ └───────────────────────┘ └──────────────┘
src └────┘└────────┘└┘└──────┘└┘└──────────┘└┘└───────────────────────┘└┘└──────────────┘└─
typ └────┘└────────┘└┘└──────┘└┘└──────────┘└┘└───────────────────────┘└┘└──────────────┘└─
doc └────┘└────────┘└┘ └┘ └┘└───────────────────────┘└┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────────────────
403
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
404 lemma integrable_to_fun (f : α →ₘ β) : integrable f ↔ (measure_theory.integrable f.to_fun) :=
id ┴ └┘ ┴ └────────┘ ┴ ┴ └───────────────────────┘ ┴└─────┘
src └┘ └────────┘ ┴ └───────────────────────┘ └─────┘
typ ┴ └┘ ┴ └────────┘ ┴ ┴ └───────────────────────┘ ┴└─────┘
doc └┘ └────────┘ └───────────────────────┘ └─────┘
405 by conv_lhs { rw [self_eq_mk f, integrable_mk] }
id └────────┘ ┴ └───────────┘
src └─────────┘└──┘└────────┘┴ └┘└───────────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└───────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└─────────────┘ ┴┴└
406
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
407 local attribute [simp] integrable_mk
id └───────────┘
src └───────────┘
typ └───────────┘
doc └──┘
408
409 lemma integrable_zero : integrable (0 : α →ₘ β) := mem_ball_self coe_lt_top
id └────────┘ ┴ └┘ ┴ └───────────┘ └────────┘
src └────────┘ └┘ └───────────┘ └────────┘
typ └────────┘ ┴ └┘ ┴ └───────────┘ └────────┘
doc └────────┘ └┘
410
411 lemma integrable.add : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f + g) :=
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
src └┘ └────────┘ └────────┘ └────────┘ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
doc └┘ └────────┘ └────────┘ └────────┘
412 begin
st └─────
413 rintros ⟨f, hf⟩ ⟨g, hg⟩,
src └─────────────────────┘
typ └─────────────────────┘
doc └─────────────────────┘
txt └─────────────────────┘
par └─────────────────────┘
pid └──────────────┘
st ────────────────────────┘└─
414 simp only [mem_ball, zero_def, mk_add_mk, integrable_mk, quot_mk_eq_mk],
id └──────┘ └──────┘ └───────┘ └───────────┘ └───────────┘
src └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘┴
typ └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
415 assume hfi hgi,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
416 exact hfi.add hf hg hgi
id └─────┘ └┘ └┘ └─┘
src └────┘└─────┘┴ ┴ ┴ ┴
typ └────┘└─────┘┴└┘┴└┘┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────┘
417 end
st └─┘
418
419 lemma integrable.neg : ∀ {f : α →ₘ β}, integrable f → integrable (-f) :=
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴┴
src └┘ └────────┘ └────────┘ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴┴
doc └┘ └────────┘ └────────┘
420 by { rintros ⟨f, hf⟩, have := measure_theory.integrable.neg, simpa }
id └───────────────────────────┘
src └─────────────┘ └──────┘└───────────────────────────┘ └────┘
typ └─────────────┘ └──────┘└───────────────────────────┘ └────┘
doc └─────────────┘ └──────┘ └────┘
txt └─────────────┘ └──────┘ └────┘
par └─────────────┘ └──────┘ └────┘
pid └──────┘ └───┘└─┘ ┴
st └────────────────┘└─────────────────────────────────────┘└──────┘└┘
421
422 lemma integrable.sub : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f - g) :=
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
src └┘ └────────┘ └────────┘ └────────┘ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
doc └┘ └────────┘ └────────┘ └────────┘
423 begin
st └─────
424 rintros ⟨f, hfm⟩ ⟨g, hgm⟩,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └────────────────┘
st ──────────────────────────┘└─
425 simp only [mem_ball, zero_def, mk_sub_mk, integrable_mk, quot_mk_eq_mk],
id └──────┘ └──────┘ └───────┘ └───────────┘ └───────────┘
src └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘┴
typ └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
426 assume hfi hgi,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
427 exact hfi.sub hfm hgm hgi
id └─────┘ └─┘ └─┘ └─┘
src └────┘└─────┘┴ ┴ ┴ ┴
typ └────┘└─────┘┴└─┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────────┘
428 end
st └─┘
429
430 protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ β) ⊤) :=
id └─────────────┘ └──┘ ┴ └┘ ┴ ┴
src └─────────────┘ └──┘ └┘ ┴
typ └─────────────┘ └──┘ ┴ └┘ ┴ ┴
doc └─────────────┘ └──┘ └┘
431 { zero_mem := integrable_zero,
id └─────────────┘
src └─────────────┘
typ └─────────────┘
432 add_mem := λ _ _, integrable.add,
id ┴ ┴ └────────────┘
src └────────────┘
typ ┴ ┴ └────────────┘
433 neg_mem := λ _, integrable.neg }
id ┴ └────────────┘
src └────────────┘
typ ┴ └────────────┘
434
435 section normed_space
436 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
437
438 lemma integrable.smul : ∀ {c : 𝕜} {f : α →ₘ β}, integrable f → integrable (c • f) :=
id ┴ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
src └┘ └────────┘ └────────┘ ┴
typ ┴ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
doc └┘ └────────┘ └────────┘
439 by { assume c, rintros ⟨f, hf⟩, simpa using integrable.smul _ }
id └─────────────┘
src └──────┘ └─────────────┘ └──────────┘└─────────────┘└─┘
typ └──────┘ └─────────────┘ └──────────┘└─────────────┘└─┘
doc └──────┘ └─────────────┘ └──────────┘ └─┘
txt └──────┘ └─────────────┘ └──────────┘ └─┘
par └──────┘ └─────────────┘ └──────────┘ └─┘
pid └──────┘ └──────┘ ┴└────┘ └┘┴
st └─────────┘└───────────────┘└──────────────────────────────┘└┘
440
441 end normed_space
442
443 end ae_eq_fun
444
445 section
446 variables (α β)
447
448 /-- The space of equivalence classes of integrable (and measurable) functions, where two integrable
449 functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure
450 `0`. -/
451 def l1 : Type (max u v) := subtype (@ae_eq_fun.integrable α _ β _ _)
id └─────┘ └──────────────────┘ ┴ ┴
src └─────┘ └──────────────────┘
typ └─────┘ └──────────────────┘ ┴ ┴
doc └──────────────────┘
452
453 infixr ` →₁ `:25 := l1
id └┘
src └┘
typ └┘
doc └┘
454
455 end
456
457 namespace l1
458 open ae_eq_fun
459 local attribute [instance] ae_eq_fun.is_add_subgroup
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
460
461 instance : has_coe (α →₁ β) (α →ₘ β) := ⟨subtype.val⟩
id └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ └─────────┘
src └─────┘ └┘ └┘ └─────────┘
typ └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ └─────────┘
doc └┘ └┘
462
463 protected lemma eq {f g : α →₁ β} : (f : α →ₘ β) = (g : α →ₘ β) → f = g := subtype.eq
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘
src └┘ └┘ ┴ └┘ ┴ └────────┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘
doc └┘ └┘ └┘
464 @[elim_cast] protected lemma eq_iff {f g : α →₁ β} : (f : α →ₘ β) = (g : α →ₘ β) ↔ f = g :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └┘ └┘ └┘
465 iff.intro (l1.eq) (congr_arg coe)
id └───────┘ └───┘ └───────┘ └─┘
src └───────┘ └───┘ └───────┘ └─┘
typ └───────┘ └───┘ └───────┘ └─┘
466
467 /- TODO : order structure of l1-/
468
469 /-- `L¹` space forms a `emetric_space`, with the emetric being inherited from almost everywhere
470 functions, i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`. -/
471 instance : emetric_space (α →₁ β) := subtype.emetric_space
id └───────────┘ ┴ └┘ ┴ └───────────────────┘
src └───────────┘ └┘ └───────────────────┘
typ └───────────┘ ┴ └┘ ┴ └───────────────────┘
doc └───────────┘ └┘ └───────────────────┘
472
473 /-- `L¹` space forms a `metric_space`, with the metric being inherited from almost everywhere
474 functions, i.e., `edist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a))`. -/
475 instance : metric_space (α →₁ β) := metric_space_emetric_ball 0 ⊤
id └──────────┘ ┴ └┘ ┴ └───────────────────────┘ ┴
src └──────────┘ └┘ └───────────────────────┘ ┴
typ └──────────┘ ┴ └┘ ┴ └───────────────────────┘ ┴
doc └──────────┘ └┘ └───────────────────────┘
476 instance : add_comm_group (α →₁ β) := subtype.add_comm_group
id └────────────┘ ┴ └┘ ┴ └────────────────────┘
src └────────────┘ └┘ └────────────────────┘
typ └────────────┘ ┴ └┘ ┴ └────────────────────┘
doc └┘
477
478 instance : inhabited (α →₁ β) := ⟨0⟩
id └───────┘ ┴ └┘ ┴
src └───────┘ └┘
typ └───────┘ ┴ └┘ ┴
doc └┘
479
480 @[simp, elim_cast] lemma coe_zero : ((0 : α →₁ β) : α →ₘ β) = 0 := rfl
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘
src └┘ └┘ ┴ └─┘
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘
doc └──┘ └───────┘ └┘ └┘
481 @[simp, move_cast] lemma coe_add (f g : α →₁ β) : ((f + g : α →₁ β) : α →ₘ β) = f + g := rfl
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ └┘ └┘ ┴ ┴ └─┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───────┘ └┘ └┘ └┘
482 @[simp, move_cast] lemma coe_neg (f : α →₁ β) : ((-f : α →₁ β) : α →ₘ β) = -f := rfl
id ┴ └┘ ┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─┘
src └┘ ┴ └┘ └┘ ┴ ┴ └─┘
typ ┴ └┘ ┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─┘
doc └──┘ └───────┘ └┘ └┘ └┘
483 @[simp, move_cast] lemma coe_sub (f g : α →₁ β) : ((f - g : α →₁ β) : α →ₘ β) = f - g := rfl
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ └┘ └┘ ┴ ┴ └─┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───────┘ └┘ └┘ └┘
484 @[simp] lemma edist_eq (f g : α →₁ β) : edist f g = edist (f : α →ₘ β) (g : α →ₘ β) := rfl
id ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └┘ └───┘ ┴ └───┘ └┘ └┘ └─┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └┘ └┘ └┘
485
486 lemma dist_eq (f g : α →₁ β) : dist f g = ennreal.to_real (edist (f : α →ₘ β) (g : α →ₘ β)) := rfl
id ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └┘ └──┘ ┴ └─────────────┘ └───┘ └┘ └┘ └─┘
typ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └┘ └─────────────┘ └┘ └┘
487
488 /-- The norm on `L¹` space is defined to be `∥f∥ = ∫⁻ a, edist (f a) 0`. -/
489 instance : has_norm (α →₁ β) := ⟨λ f, dist f 0⟩
id └──────┘ ┴ └┘ ┴ ┴ └──┘ ┴
src └──────┘ └┘ └──┘
typ └──────┘ ┴ └┘ ┴ ┴ └──┘ ┴
doc └──────┘ └┘
490
491 lemma norm_eq (f : α →₁ β) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ β) 0) := rfl
id ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ └─┘
src └┘ ┴ ┴ ┴ └─────────────┘ └───┘ └┘ └─┘
typ ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ └─┘
doc └┘ └─────────────┘ └┘
492
493 instance : normed_group (α →₁ β) := normed_group.of_add_dist (λ x, rfl) $ by
id └──────────┘ ┴ └┘ ┴ └──────────────────────┘ ┴ └─┘
src └──────────┘ └┘ └──────────────────────┘ └─┘
typ └──────────┘ ┴ └┘ ┴ └──────────────────────┘ ┴ └─┘
doc └──────────┘ └┘ └──────────────────────┘
st └
494 { intros, simp only [dist_eq, coe_add], rw edist_eq_add_add }
id └─────┘ └─────┘ └──────────────┘
src └────┘ └─────────┘└─────┘└┘└─────┘┴ └─┘└──────────────┘┴
typ └────┘ └─────────┘└─────┘└┘└─────┘┴ └─┘└──────────────┘┴
doc └────┘ └─────────┘ └┘ ┴ └─┘ ┴
txt └────┘ └─────────┘ └┘ ┴ └─┘ ┴
par └────┘ └─────────┘ └┘ ┴ └─┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st ───────┘└────────────────────────────┘└────────────────────┘└┘
495
496 section normed_space
497
498 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
499
500 instance : has_scalar 𝕜 (α →₁ β) := ⟨λ x f, ⟨x • (f : α →ₘ β), ae_eq_fun.integrable.smul f.2⟩⟩
id └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────────────────────┘ ┴┴
src └────────┘ └┘ ┴ └┘ └───────────────────────┘ ┴
typ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────────────────────┘ ┴┴
doc └────────┘ └┘ └┘
501
502 @[simp, move_cast] lemma coe_smul (c : 𝕜) (f : α →₁ β) :
id ┴ ┴ └┘ ┴
src └┘
typ ┴ ┴ └┘ ┴
doc └──┘ └───────┘ └┘
503 ((c • f : α →₁ β) : α →ₘ β) = c • (f : α →ₘ β) := rfl
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ └┘ └┘ ┴ ┴ └┘ └─┘
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └┘ └┘ └┘
504
505 instance : semimodule 𝕜 (α →₁ β) :=
id └────────┘ ┴ ┴ └┘ ┴
src └────────┘ └┘
typ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘
506 { one_smul := λf, l1.eq (by { simp only [coe_smul], exact one_smul _ _ }),
id ┴ └───┘ └──────┘ └──────┘
src └───┘ └─────────┘└──────┘┴ └────┘└──────┘└───┘
typ ┴ └───┘ └─────────┘└──────┘┴ └────┘└──────┘└───┘
doc └─────────┘ ┴ └────┘ └───┘
txt └─────────┘ ┴ └────┘ └───┘
par └─────────┘ ┴ └────┘ └───┘
pid ┴└──┘└┘ ┴ ┴ └──┘┴
st └─────────────────────┘└───────────────────┘└┘
507 mul_smul := λx y f, l1.eq (by { simp only [coe_smul], exact mul_smul _ _ _ }),
id ┴ ┴ ┴ └───┘ └──────┘ └──────┘
src └───┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └───┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ ┴ └────┘ └─────┘
txt └─────────┘ ┴ └────┘ └─────┘
par └─────────┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ ┴ ┴ └────┘┴
st └─────────────────────┘└─────────────────────┘└┘
508 smul_add := λx f g, l1.eq (by { simp only [coe_smul, coe_add], exact smul_add _ _ _ }),
id ┴ ┴ ┴ └───┘ └──────┘ └─────┘ └──────┘
src └───┘ └─────────┘└──────┘└┘└─────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └───┘ └─────────┘└──────┘└┘└─────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ └┘ ┴ └────┘ └─────┘
txt └─────────┘ └┘ ┴ └────┘ └─────┘
par └─────────┘ └┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ └┘ ┴ ┴ └────┘┴
st └──────────────────────────────┘└─────────────────────┘└┘
509 smul_zero := λx, l1.eq (by { simp only [coe_zero, coe_smul], exact smul_zero _ }),
id ┴ └───┘ └──────┘ └──────┘ └───────┘
src └───┘ └─────────┘└──────┘└┘└──────┘┴ └────┘└───────┘└─┘
typ ┴ └───┘ └─────────┘└──────┘└┘└──────┘┴ └────┘└───────┘└─┘
doc └─────────┘ └┘ ┴ └────┘ └─┘
txt └─────────┘ └┘ ┴ └────┘ └─┘
par └─────────┘ └┘ ┴ └────┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴ └┘┴
st └───────────────────────────────┘└──────────────────┘└┘
510 add_smul := λx y f, l1.eq (by { simp only [coe_smul], exact add_smul _ _ _ }),
id ┴ ┴ ┴ └───┘ └──────┘ └──────┘
src └───┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └───┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ ┴ └────┘ └─────┘
txt └─────────┘ ┴ └────┘ └─────┘
par └─────────┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ ┴ ┴ └────┘┴
st └─────────────────────┘└─────────────────────┘└┘
511 zero_smul := λf, l1.eq (by { simp only [coe_smul], exact zero_smul _ _ }) }
id ┴ └───┘ └──────┘ └───────┘
src └───┘ └─────────┘└──────┘┴ └────┘└───────┘└───┘
typ ┴ └───┘ └─────────┘└──────┘┴ └────┘└───────┘└───┘
doc └─────────┘ ┴ └────┘ └───┘
txt └─────────┘ ┴ └────┘ └───┘
par └─────────┘ ┴ └────┘ └───┘
pid ┴└──┘└┘ ┴ ┴ └──┘┴
st └─────────────────────┘└────────────────────┘└┘
512
513 instance : module 𝕜 (α →₁ β) := { .. l1.semimodule }
id └────┘ ┴ ┴ └┘ ┴ └───────────┘
src └────┘ └┘ └───────────┘
typ └────┘ ┴ ┴ └┘ ┴ └───────────┘
doc └────┘ └┘
514
515 instance : vector_space 𝕜 (α →₁ β) := { .. l1.semimodule }
id └──────────┘ ┴ ┴ └┘ ┴ └───────────┘
src └──────────┘ └┘ └───────────┘
typ └──────────┘ ┴ ┴ └┘ ┴ └───────────┘
doc └──────────┘ └┘
516
517 instance : normed_space 𝕜 (α →₁ β) :=
id └──────────┘ ┴ ┴ └┘ ┴
src └──────────┘ └┘
typ └──────────┘ ┴ ┴ └┘ ┴
doc └──────────┘ └┘
518 ⟨ begin
st └─────
519 rintros x ⟨f, hf⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ────────────────────┘└─
520 show ennreal.to_real (edist (x • f) 0) = ∥x∥ * ennreal.to_real (edist f 0),
id ┴ ┴ ┴┴┴ ┴ └─────────────┘ └───┘ ┴
src └───┘ ┴ ┴ ┴┴┴ └───┘┴┴┴ ┴┴┴┴└─────────────┘┴ └───┘┴ └─┘
typ └───┘ ┴ ┴ ┴┴┴ └───┘┴┴┴┴┴┴┴┴└─────────────┘┴ └───┘┴┴└─┘
doc └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴└─────────────┘┴ ┴ └─┘
txt └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
par └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
pid └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
521 rw [edist_smul, to_real_of_real_mul],
id └────────┘ └─────────────────┘
src └──┘└────────┘└┘└─────────────────┘┴
typ └──┘└────────┘└┘└─────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────┘└───────────────────┘└──
522 exact norm_nonneg _
id └─────────┘
src └────┘└─────────┘└──
typ └────┘└─────────┘└──
doc └────┘ └──
txt └────┘ └──
par └────┘ └──
pid ┴ └┘└
st ────────────────────────
523 end ⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
524
525 end normed_space
526
527 section of_fun
528
529 /-- Construct the equivalence class `[f]` of a measurable and integrable function `f`. -/
530 def of_fun (f : α → β) (hfm : measurable f) (hfi : integrable f) : (α →₁ β) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ └┘ ┴
src └────────┘ └────────┘ └┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └────────┘ └┘
531 ⟨mk f hfm, by { rw integrable_mk, exact hfi }⟩
id └┘ ┴ └─┘ └───────────┘ └─┘
src └┘ └─┘└───────────┘ └────┘ ┴
typ └┘ ┴ └─┘ └─┘└───────────┘ └────┘└─┘┴
doc └┘ └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────────────┘└──────────┘└┘
532
533 lemma of_fun_eq_mk (f : α → β) (hfm hfi) : (of_fun f hfm hfi : α →ₘ β) = mk f hfm := rfl
id ┴ ┴ └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘
src └────┘ └┘ ┴ └┘ └─┘
typ ┴ ┴ └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘
doc └────┘ └┘ └┘
534
535 lemma of_fun_eq_of_fun (f g : α → β) (hfm hfi hgm hgi) :
id ┴ ┴
typ ┴ ┴
536 of_fun f hfm hfi = of_fun g hgm hgi ↔ ∀ₘ a, f a = g a :=
id └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ └┘ ┴ ┴
typ └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────┘ └┘ ┴
537 by { rw ← l1.eq_iff, simp only [of_fun_eq_mk, mk_eq_mk] }
id └───────┘ └──────────┘ └──────┘
src └───┘└───────┘ └─────────┘└──────────┘└┘└──────┘└┘
typ └───┘└───────┘ └─────────┘└──────────┘└┘└──────┘└┘
doc └───┘ └─────────┘ └┘ └┘
txt └───┘ └─────────┘ └┘ └┘
par └───┘ └─────────┘ └┘ └┘
pid └─┘ ┴└──┘└┘ └┘ ┴┴
st └───────────────┘└───────────────────────────────────┘└┘
538
539 lemma of_fun_zero :
540 of_fun (λa:α, (0:β)) (@measurable_const _ _ _ _ (0:β)) (integrable_zero α β) = 0 := rfl
id └────┘ ┴ ┴ └──────────────┘ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
src └────┘ └──────────────┘ └─────────────┘ ┴ └─┘
typ └────┘ ┴ ┴ └──────────────┘ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
doc └────┘
541
542 lemma of_fun_add (f g : α → β) (hfm hfi hgm hgi) :
id ┴ ┴
typ ┴ ┴
543 of_fun (λa, f a + g a) (measurable.add hfm hgm) (integrable.add hfm hfi hgm hgi)
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └─┘ └────────────┘ └─┘ └─┘ └─┘ └─┘
src └────┘ ┴ └────────────┘ └────────────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └─┘ └────────────┘ └─┘ └─┘ └─┘ └─┘
doc └────┘
544 = of_fun f hfm hfi + of_fun g hgm hgi :=
id ┴ └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘
src ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘
doc └────┘ └────┘
545 rfl
id └─┘
src └─┘
typ └─┘
546
547 lemma of_fun_neg (f : α → β) (hfm hfi) :
id ┴ ┴
typ ┴ ┴
548 of_fun (λa, - f a) (measurable.neg hfm) (integrable.neg hfi) = - of_fun f hfm hfi := rfl
id └────┘ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └────────────┘ └─┘ ┴ ┴ └────┘ ┴ └─┘ └─┘ └─┘
src └────┘ ┴ └────────────┘ └────────────┘ ┴ ┴ └────┘ └─┘
typ └────┘ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └────────────┘ └─┘ ┴ ┴ └────┘ ┴ └─┘ └─┘ └─┘
doc └────┘ └────┘
549
550 lemma of_fun_sub (f g : α → β) (hfm hfi hgm hgi) :
id ┴ ┴
typ ┴ ┴
551 of_fun (λa, f a - g a) (measurable.sub hfm hgm) (integrable.sub hfm hfi hgm hgi)
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └─┘ └────────────┘ └─┘ └─┘ └─┘ └─┘
src └────┘ ┴ └────────────┘ └────────────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └─┘ └────────────┘ └─┘ └─┘ └─┘ └─┘
doc └────┘
552 = of_fun f hfm hfi - of_fun g hgm hgi :=
id ┴ └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘
src ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ └─┘ └─┘ ┴ └────┘ ┴ └─┘ └─┘
doc └────┘ └────┘
553 rfl
id └─┘
src └─┘
typ └─┘
554
555 lemma norm_of_fun (f : α → β) (hfm hfi) : ∥of_fun f hfm hfi∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) :=
id ┴ ┴ ┴└────┘ ┴ └─┘ └─┘┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴ ┴
src ┴└────┘ ┴ ┴ └─────────────┘ └┘ ┴ └───┘
typ ┴ ┴ ┴└────┘ ┴ └─┘ └─┘┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴ ┴
doc └────┘ └─────────────┘ └┘ ┴
556 rfl
id └─┘
src └─┘
typ └─┘
557
558 lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hfm hfi) :
id ┴ ┴
typ ┴ ┴
559 ∥of_fun f hfm hfi∥ = ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
id ┴└────┘ ┴ └─┘ └─┘┴ ┴ └─────────────┘ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴
src ┴└────┘ ┴ ┴ └─────────────┘ └┘ ┴ └─────────────┘ ┴ ┴
typ ┴└────┘ ┴ └─┘ └─┘┴ ┴ └─────────────┘ └┘ ┴┴ └─────────────┘ ┴┴ ┴┴
doc └────┘ └─────────────┘ └┘ ┴ └─────────────┘
560 by { rw [norm_of_fun, lintegral_norm_eq_lintegral_edist] }
id └─────────┘ └───────────────────────────────┘
src └──┘└─────────┘└┘└───────────────────────────────┘└┘
typ └──┘└─────────┘└┘└───────────────────────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └────────────────┘└─────────────────────────────────┘┴┴└┘
561
562 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
563
564 lemma of_fun_smul (f : α → β) (hfm hfi) (k : 𝕜) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
565 of_fun (λa, k • f a) (measurable.smul _ hfm) (integrable.smul _ hfi) = k • of_fun f hfm hfi := rfl
id └────┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └─┘ └─────────────┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └─┘ └─┘ └─┘
src └────┘ ┴ └─────────────┘ └─────────────┘ ┴ ┴ └────┘ └─┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └─┘ └─────────────┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └─┘ └─┘ └─┘
doc └────┘ └────┘
566
567 end of_fun
568
569 section to_fun
570
571 /-- Find a representative of a `L¹` function [f] -/
572 @[reducible]
doc └───────┘
573 protected def to_fun (f : α →₁ β) : α → β := (f : α →ₘ β).to_fun
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────┘
src └┘ └┘ └────┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────┘
doc └┘ └┘ └────┘
574
575 protected lemma measurable (f : α →₁ β) : measurable f.to_fun := f.1.measurable
id ┴ └┘ ┴ └────────┘ ┴└─────┘ ┴┴ └────────┘
src └┘ └────────┘ └─────┘ ┴ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴└─────┘ ┴┴ └────────┘
doc └┘ └────────┘ └─────┘
576
577 protected lemma integrable (f : α →₁ β) : integrable f.to_fun :=
id ┴ └┘ ┴ └────────┘ ┴└─────┘
src └┘ └────────┘ └─────┘
typ ┴ └┘ ┴ └────────┘ ┴└─────┘
doc └┘ └────────┘ └─────┘
578 by { rw [l1.to_fun, ← integrable_to_fun], exact f.2 }
id └───────┘ └───────────────┘ ┴
src └──┘└───────┘└──┘└───────────────┘┴ └────┘ └─┘
typ └──┘└───────┘└──┘└───────────────┘┴ └────┘┴└─┘
doc └──┘└───────┘└──┘ ┴ └────┘ └─┘
txt └──┘ └──┘ ┴ └────┘ └─┘
par └──┘ └──┘ ┴ └────┘ └─┘
pid └┘ └──┘ ┴ ┴ └─┘
st └──────────────┘└───────────────────┘└───────────┘└┘
579
580 lemma of_fun_to_fun (f : α →₁ β) : of_fun (f.to_fun) f.measurable f.integrable = f :=
id ┴ └┘ ┴ └────┘ ┴└─────┘ ┴└─────────┘ ┴└─────────┘ ┴ ┴
src └┘ └────┘ └─────┘ └─────────┘ └─────────┘ ┴
typ ┴ └┘ ┴ └────┘ ┴└─────┘ ┴└─────────┘ ┴└─────────┘ ┴ ┴
doc └┘ └────┘ └─────┘
581 begin
st └─────
582 rcases f with ⟨f, hfi⟩,
id ┴
src └─────┘ └────────────┘
typ └─────┘┴└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ───────────────────────┘└─
583 rw [of_fun, subtype.mk_eq_mk],
id └────┘ └──────────────┘
src └──┘└────┘└┘└──────────────┘┴
typ └──┘└────┘└┘└──────────────┘┴
doc └──┘└────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────┘└────────────────┘└──
584 exact (self_eq_mk f).symm
id └────────┘ ┴
src └────┘ └────────┘┴ └─────┘
typ └────┘ └────────┘┴┴└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ───────────────────────────┘
585 end
st └─┘
586
587 lemma mk_to_fun (f : α →₁ β) : mk (f.to_fun) f.measurable = f :=
id ┴ └┘ ┴ └┘ ┴└─────┘ ┴└─────────┘ ┴ ┴
src └┘ └┘ └─────┘ └─────────┘ ┴
typ ┴ └┘ ┴ └┘ ┴└─────┘ ┴└─────────┘ ┴ ┴
doc └┘ └┘ └─────┘
588 by { rw ← of_fun_eq_mk, rw l1.eq_iff, exact of_fun_to_fun f }
id └──────────┘ └───────┘ └───────────┘ ┴
src └───┘└──────────┘ └─┘└───────┘ └────┘└───────────┘┴ ┴
typ └───┘└──────────┘ └─┘└───────┘ └────┘└───────────┘┴┴┴
doc └───┘ └─┘ └────┘ ┴ ┴
txt └───┘ └─┘ └────┘ ┴ ┴
par └───┘ └─┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴ ┴
st └──────────────────┘└────────────┘└──────────────────────┘└┘
589
590 lemma to_fun_of_fun (f : α → β) (hfm hfi) : ∀ₘ a, (of_fun f hfm hfi).to_fun a = f a :=
id ┴ ┴ └┘ ┴┴ └────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ ┴ ┴
src └┘ ┴ └────┘ └────┘ ┴
typ ┴ ┴ └┘ ┴┴ └────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └────┘ └────┘
591 begin
st └─────
592 filter_upwards [all_ae_mk_to_fun f hfm],
id └──────────────┘ ┴ └─┘
src └──────────────┘└──────────────┘┴ ┴ ┴
typ └──────────────┘└──────────────┘┴┴┴└─┘┴
doc └──────────────┘ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st ────────────────────────────────────────┘└─
593 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
594 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
595 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
596 rw ← h,
id ┴
src └───┘
typ └───┘┴
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────┘└─
597 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
598 end
st └─┘
599
600 variables (α β)
601 lemma zero_to_fun : ∀ₘ a, (0 : α →₁ β).to_fun a = 0 := ae_eq_fun.zero_to_fun
id └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └───────────────────┘
src └┘ ┴ └┘ └────┘ ┴ └───────────────────┘
typ └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └───────────────────┘
doc └┘ ┴ └┘ └────┘
602 variables {α β}
603
604 lemma add_to_fun (f g : α →₁ β) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
id ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘ └─────┘
605 ae_eq_fun.add_to_fun _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
606
607 lemma neg_to_fun (f : α →₁ β) : ∀ₘ a, (-f).to_fun a = -f.to_fun a := ae_eq_fun.neg_to_fun _
id ┴ └┘ ┴ └┘ ┴┴ ┴┴ └────┘ ┴ ┴ ┴┴└─────┘ ┴ └──────────────────┘
src └┘ └┘ ┴ ┴ └────┘ ┴ ┴ └─────┘ └──────────────────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴┴ └────┘ ┴ ┴ ┴┴└─────┘ ┴ └──────────────────┘
doc └┘ └┘ ┴ └────┘ └─────┘
608
609 lemma sub_to_fun (f g : α →₁ β) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a :=
id ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘ └─────┘
610 ae_eq_fun.sub_to_fun _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
611
612 lemma dist_to_fun (f g : α →₁ β) : dist f g = ennreal.to_real (∫⁻ x, edist (f.to_fun x) (g.to_fun x)) :=
id ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
src └┘ └──┘ ┴ └─────────────┘ └┘ ┴ └───┘ └─────┘ └─────┘
typ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
doc └┘ └─────────────┘ └┘ ┴ └─────┘ └─────┘
613 by { simp only [dist_eq, edist_to_fun] }
id └─────┘ └──────────┘
src └─────────┘└─────┘└┘└──────────┘└┘
typ └─────────┘└─────┘└┘└──────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st └───────────────────────────────────┘└┘
614
615 lemma norm_eq_nnnorm_to_fun (f : α →₁ β) : ∥f∥ = ennreal.to_real (∫⁻ a, nnnorm (f.to_fun a)) :=
id ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └┘ ┴┴ └────┘ ┴└─────┘ ┴
src └┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴ └────┘ └─────┘
typ ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └┘ ┴┴ └────┘ ┴└─────┘ ┴
doc └┘ └─────────────┘ └┘ ┴ └────┘ └─────┘
616 by { rw [lintegral_nnnorm_eq_lintegral_edist, ← edist_zero_to_fun], refl }
id └─────────────────────────────────┘ └───────────────┘
src └──┘└─────────────────────────────────┘└──┘└───────────────┘┴ └───┘
typ └──┘└─────────────────────────────────┘└──┘└───────────────┘┴ └───┘
doc └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ ┴ ┴
st └────────────────────────────────────────┘└───────────────────┘└──────┘└┘
617
618 lemma norm_eq_norm_to_fun (f : α →₁ β) : ∥f∥ = ennreal.to_real (∫⁻ a, ennreal.of_real ∥f.to_fun a∥) :=
id ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └┘ ┴┴ └─────────────┘ ┴┴└─────┘ ┴┴
src └┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴ └─────────────┘ ┴ └─────┘ ┴
typ ┴ └┘ ┴ ┴┴┴ ┴ └─────────────┘ └┘ ┴┴ └─────────────┘ ┴┴└─────┘ ┴┴
doc └┘ └─────────────┘ └┘ ┴ └─────────────┘ └─────┘
619 by { rw norm_eq_nnnorm_to_fun, congr, funext, rw of_real_norm_eq_coe_nnnorm }
id └───────────────────┘ └────────────────────────┘
src └─┘└───────────────────┘ └───┘ └────┘ └─┘└────────────────────────┘┴
typ └─┘└───────────────────┘ └───┘ └────┘ └─┘└────────────────────────┘┴
doc └─┘ └────┘ └─┘ ┴
txt └─┘ └───┘ └────┘ └─┘ ┴
par └─┘ └───┘ └────┘ └─┘ ┴
pid ┴ ┴ ┴
st └─────────────────────────┘└─────┘└──────┘└──────────────────────────────┘└┘
620
621 lemma lintegral_edist_to_fun_lt_top (f g : α →₁ β) : (∫⁻ a, edist (f.to_fun a) (g.to_fun a)) < ⊤ :=
id ┴ └┘ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴ ┴ ┴
src └┘ └┘ ┴ └───┘ └─────┘ └─────┘ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴ ┴ ┴
doc └┘ └┘ ┴ └─────┘ └─────┘
622 begin
st └─────
623 apply lintegral_edist_lt_top,
id └────────────────────┘
src └────┘└────────────────────┘
typ └────┘└────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
624 exact f.measurable, exact f.integrable, exact g.measurable, exact g.integrable
id └──────────┘ └──────────┘ └──────────┘ └──────────┘
src └────┘└──────────┘ └────┘└──────────┘ └────┘└──────────┘ └────┘└──────────┘┴
typ └────┘└──────────┘ └────┘└──────────┘ └────┘└──────────┘ └────┘└──────────┘┴
doc └────┘ └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────┘└──────────────────┘└──────────────────┘└───────────────────┘
625 end
st └─┘
626
627 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
628
629 lemma smul_to_fun (c : 𝕜) (f : α →₁ β) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
id ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
typ ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘
630 ae_eq_fun.smul_to_fun _ _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
631
632 end to_fun
633
634 section pos_part
635
636 /-- Positive part of a function in `L¹` space. -/
637 def pos_part (f : α →₁ ℝ) : α →₁ ℝ :=
id ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
638 ⟨ ae_eq_fun.pos_part f,
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
doc └────────────────┘
639 begin
st └─────
640 rw [ae_eq_fun.integrable_to_fun, integrable_congr_ae (pos_part_to_fun _)],
id └─────────────────────────┘ └─────────────────┘ └─────────────┘
src └──┘└─────────────────────────┘└┘└─────────────────┘┴ └─────────────┘└──┘
typ └──┘└─────────────────────────┘└┘└─────────────────┘┴ └─────────────┘└──┘
doc └──┘ └┘ ┴ └──┘
txt └──┘ └┘ ┴ └──┘
par └──┘ └┘ ┴ └──┘
pid └┘ └┘ ┴ └──┘
st ──────────────────────────────────┘└───────────────────────────────────────┘└──
641 exact integrable.max_zero f.integrable
id └─────────────────┘ └──────────┘
src └────┘└─────────────────┘┴└──────────┘└
typ └────┘└─────────────────┘┴└──────────┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────────────────────
642 end ⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
643
644 /-- Negative part of a function in `L¹` space. -/
645 def neg_part (f : α →₁ ℝ) : α →₁ ℝ := pos_part (-f)
id ┴ └┘ ┴ ┴ └┘ ┴ └──────┘ ┴┴
src └┘ ┴ └┘ ┴ └──────┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ └──────┘ ┴┴
doc └┘ └┘ └──────┘
646
647 @[move_cast] lemma coe_pos_part (f : α →₁ ℝ) : (f.pos_part : α →ₘ ℝ) = (f : α →ₘ ℝ).pos_part := rfl
id ┴ └┘ ┴ ┴└───────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘
src └┘ ┴ └───────┘ └┘ ┴ ┴ └┘ ┴ └──────┘ └─┘
typ ┴ └┘ ┴ ┴└───────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘
doc └───────┘ └┘ └───────┘ └┘ └┘ └──────┘
648
649 lemma pos_part_to_fun (f : α →₁ ℝ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) 0 :=
id ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴└─────┘ ┴
src └┘ ┴ └┘ ┴ └──────┘ └────┘ ┴ └─┘ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴└─────┘ ┴
doc └┘ └┘ ┴ └──────┘ └────┘ └─────┘
650 ae_eq_fun.pos_part_to_fun _
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
651
652 lemma neg_part_to_fun_eq_max (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = max (- f.to_fun a) 0 :=
id ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴└─────┘ ┴
src └┘ ┴ └┘ ┴ └──────┘ └────┘ ┴ └─┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └──────┘ └────┘ └─────┘
653 begin
st └─────
654 rw neg_part,
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘└──────┘
txt └─┘
par └─┘
pid ┴
st ────────────┘└─
655 filter_upwards [pos_part_to_fun (-f), neg_to_fun f],
id └─────────────┘ ┴┴ └────────┘ ┴
src └──────────────┘└─────────────┘┴ ┴ └─┘└────────┘┴ ┴
typ └──────────────┘└─────────────┘┴ ┴┴└─┘└────────┘┴┴┴
doc └──────────────┘ ┴ └─┘ ┴ ┴
txt └──────────────┘ ┴ └─┘ ┴ ┴
par └──────────────┘ ┴ └─┘ ┴ ┴
pid └┘ ┴ └─┘ ┴ ┴
st ────────────────────────────────────────────────────┘└─
656 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
657 assume a h₁ h₂,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
658 rw [h₁, h₂]
id └┘ └┘
src └──┘ └┘ └┘
typ └──┘└┘└┘└┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────┘└──┘┴┴
659 end
st └─┘
660
661 lemma neg_part_to_fun_eq_min (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = - min (f.to_fun a) 0 :=
id ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴└─────┘ ┴
src └┘ ┴ └┘ ┴ └──────┘ └────┘ ┴ ┴ └─┘ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴└─────┘ ┴
doc └┘ └┘ ┴ └──────┘ └────┘ └─────┘
662 begin
st └─────
663 filter_upwards [neg_part_to_fun_eq_max f],
id └────────────────────┘ ┴
src └──────────────┘└────────────────────┘┴ ┴
typ └──────────────┘└────────────────────┘┴┴┴
doc └──────────────┘ ┴ ┴
txt └──────────────┘ ┴ ┴
par └──────────────┘ ┴ ┴
pid └┘ ┴ ┴
st ──────────────────────────────────────────┘└─
664 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
665 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
666 rw [h, min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero],
id ┴ └────────────────────┘ └────────────┘ └──────┘
src └──┘ └┘└────────────────────┘└┘└────────────┘└┘└──────┘┴
typ └──┘┴└┘└────────────────────┘└┘└────────────┘└┘└──────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ──────┘└──────────────────────┘└──────────────┘└────────┘└──
667 end
st ──┘
668
669 lemma norm_le_norm_of_ae_le {f g : α →₁ β} (h : ∀ₘ a, ∥f.to_fun a∥ ≤ ∥g.to_fun a∥) : ∥f∥ ≤ ∥g∥ :=
id ┴ └┘ ┴ └┘ ┴┴ ┴┴└─────┘ ┴┴ ┴ ┴┴└─────┘ ┴┴ ┴┴┴ ┴ ┴┴┴
src └┘ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴┴ ┴┴└─────┘ ┴┴ ┴ ┴┴└─────┘ ┴┴ ┴┴┴ ┴ ┴┴┴
doc └┘ └┘ ┴ └─────┘ └─────┘
670 begin
st └─────
671 simp only [l1.norm_eq_norm_to_fun],
id └────────────────────┘
src └─────────┘└────────────────────┘┴
typ └─────────┘└────────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───────────────────────────────────┘└─
672 rw to_real_le_to_real,
id └────────────────┘
src └─┘└────────────────┘
typ └─┘└────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
673 { apply lintegral_le_lintegral_ae,
id └───────────────────────┘
src └────┘└───────────────────────┘
typ └────┘└───────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────────────────────┘└─
674 filter_upwards [h],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ─────────────────────┘└─
675 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────────────────┘└─
676 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ─────────────┘└─
677 exact of_real_le_of_real h },
id └────────────────┘ ┴
src └────┘└────────────────┘┴ ┴
typ └────┘└────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────┘└┘└
678 { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact f.integrable },
id └───────────────┘ └─────────────────┘ └──────────┘
src └────┘└───────────────┘└──┘└─────────────────┘┴ └────┘└──────────┘┴
typ └────┘└───────────────┘└──┘└─────────────────┘┴ └────┘└──────────┘┴
doc └────┘ └──┘ ┴ └────┘ ┴
txt └────┘ └──┘ ┴ └────┘ ┴
par └────┘ └──┘ ┴ └────┘ ┴
pid └──┘ └──┘ ┴ ┴ ┴
st ───┘└─────────────────────┘└─────────────────────┘└────────────────────┘└┘└
679 { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact g.integrable }
id └───────────────┘ └─────────────────┘ └──────────┘
src └────┘└───────────────┘└──┘└─────────────────┘┴ └────┘└──────────┘┴
typ └────┘└───────────────┘└──┘└─────────────────┘┴ └────┘└──────────┘┴
doc └────┘ └──┘ ┴ └────┘ ┴
txt └────┘ └──┘ ┴ └────┘ ┴
par └────┘ └──┘ ┴ └────┘ ┴
pid └──┘ └──┘ ┴ ┴ ┴
st ──────────────────────────┘└─────────────────────┘└────────────────────┘└─
680 end
st ──┘
681
682 lemma continuous_pos_part : continuous $ λf : α →₁ ℝ, pos_part f :=
id └────────┘ ┴ └┘ ┴ └──────┘ ┴
src └────────┘ └┘ ┴ └──────┘
typ └────────┘ ┴ └┘ ┴ └──────┘ ┴
doc └────────┘ └┘ └──────┘
683 begin
st └─────
684 simp only [metric.continuous_iff],
id └───────────────────┘
src └─────────┘└───────────────────┘┴
typ └─────────┘└───────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────────┘└─
685 assume g ε hε,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ──────────────┘└─
686 use ε, use hε,
id ┴ └┘
src └──┘ └──┘
typ └──┘┴ └──┘└┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
pid ┴ ┴
st ──────┘└──────┘└─
687 simp only [dist_eq_norm],
id └──────────┘
src └─────────┘└──────────┘┴
typ └─────────┘└──────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────┘└─
688 assume f hfg,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ─────────────┘└─
689 refine lt_of_le_of_lt (norm_le_norm_of_ae_le _) hfg,
id └────────────┘ └───────────────────┘ └─┘
src └─────┘└────────────┘┴ └───────────────────┘└──┘
typ └─────┘└────────────┘┴ └───────────────────┘└──┘└─┘
doc └─────┘ ┴ └──┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ────────────────────────────────────────────────────┘└─
690 filter_upwards [l1.sub_to_fun f g, l1.sub_to_fun (pos_part f) (pos_part g),
id └───────────┘ ┴ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────────┘└───────────┘┴ ┴ └┘└───────────┘┴ ┴ └┘ └──────┘┴ └──
typ └──────────────┘└───────────┘┴┴┴┴└┘└───────────┘┴ ┴┴└┘ └──────┘┴┴└──
doc └──────────────┘ ┴ ┴ └┘ ┴ ┴ └┘ └──────┘┴ └──
txt └──────────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──
par └──────────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──
pid └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────
691 pos_part_to_fun f, pos_part_to_fun g],
id └─────────────┘ ┴ └─────────────┘ ┴
src ───┘└─────────────┘┴ └┘└─────────────┘┴ ┴
typ ───┘└─────────────┘┴┴└┘└─────────────┘┴┴┴
doc ───┘ ┴ └┘ ┴ ┴
txt ───┘ ┴ └┘ ┴ ┴
par ───┘ ┴ └┘ ┴ ┴
pid ───┘ ┴ └┘ ┴ ┴
st ────────────────────────────────────────┘└─
692 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
693 assume a h₁ h₂ h₃ h₄,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
694 simp only [real.norm_eq_abs, h₁, h₂, h₃, h₄],
id └──────────────┘ └┘ └┘ └┘ └┘
src └─────────┘└──────────────┘└┘ └┘ └┘ └┘ ┴
typ └─────────┘└──────────────┘└┘└┘└┘└┘└┘└┘└┘└┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────┘└─
695 exact abs_max_sub_max_le_abs _ _ _
id └────────────────────┘
src └────┘└────────────────────┘└─────┘
typ └────┘└────────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └────┘┴
st ────────────────────────────────────┘
696 end
st └─┘
697
698 lemma continuous_neg_part : continuous $ λf : α →₁ ℝ, neg_part f :=
id └────────┘ ┴ └┘ ┴ └──────┘ ┴
src └────────┘ └┘ ┴ └──────┘
typ └────────┘ ┴ └┘ ┴ └──────┘ ┴
doc └────────┘ └┘ └──────┘
699 have eq : (λf : α →₁ ℝ, neg_part f) = (λf : α →₁ ℝ, pos_part (-f)) := rfl,
id ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ └──────┘ ┴┴ └─┘
src └┘ ┴ └──────┘ ┴ └┘ ┴ └──────┘ ┴ └─┘
typ ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ └──────┘ ┴┴ └─┘
doc └┘ └──────┘ └┘ └──────┘
700 by { rw eq, exact continuous_pos_part.comp continuous_neg }
id └┘ └──────────────────────┘ └────────────┘
src └─┘└┘ └────┘└──────────────────────┘┴└────────────┘┴
typ └─┘└┘ └────┘└──────────────────────┘┴└────────────┘┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └──────┘└──────────────────────────────────────────────┘└┘
701
702 end pos_part
703
704 /- TODO: l1 is a complete space -/
705
706 end l1
707
708 end measure_theory